Run 141

git clone --depth 1 --branch main --single-branch https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git /var/lib/apodeixis/repos/job-927-source

Cloning into '/var/lib/apodeixis/repos/job-927-source'...

git checkout c11b254e6f158952e5194bc8ca3c61a10e700e78

fatal: reference is not a tree: c11b254e6f158952e5194bc8ca3c61a10e700e78

git fetch --depth 1 origin c11b254e6f158952e5194bc8ca3c61a10e700e78

From https://github.com/AlexKontorovich/PrimeNumberTheoremAnd
 * branch            c11b254e6f158952e5194bc8ca3c61a10e700e78 -> FETCH_HEAD

git checkout c11b254e6f158952e5194bc8ca3c61a10e700e78 (after fetch)

Note: switching to 'c11b254e6f158952e5194bc8ca3c61a10e700e78'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by switching back to a branch.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -c with the switch command. Example:

  git switch -c <new-branch-name>

Or undo this operation with:

  git switch -

Turn off this advice by setting config variable advice.detachedHead to false

HEAD is now at c11b254 feat(mertens): prove log_zeta_limit with corrected statement (#1588)

lake exe cache get

Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache
Decompressed 8459 file(s)
Already decompressed 8459 file(s)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 13 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8459 = 0%, 11 KB/s], Decompressed: 0
Downloaded: 38 file(s) [attempted 38/8459 = 0%, 29 KB/s], Decompressed: 0
Downloaded: 58 file(s) [attempted 58/8459 = 0%, 231 KB/s], Decompressed: 54
Downloaded: 82 file(s) [attempted 82/8459 = 0%, 62 KB/s], Decompressed: 79
Downloaded: 117 file(s) [attempted 117/8459 = 1%, 71 KB/s], Decompressed: 114
Downloaded: 148 file(s) [attempted 148/8459 = 1%, 521 KB/s], Decompressed: 141
Downloaded: 182 file(s) [attempted 182/8459 = 2%, 486 KB/s], Decompressed: 179
Downloaded: 216 file(s) [attempted 216/8459 = 2%, 1495 KB/s], Decompressed: 213
Downloaded: 253 file(s) [attempted 253/8459 = 2%, 113 KB/s], Decompressed: 237
Downloaded: 283 file(s) [attempted 283/8459 = 3%, 68 KB/s], Decompressed: 278
Downloaded: 320 file(s) [attempted 320/8459 = 3%, 637 KB/s], Decompressed: 316
Downloaded: 360 file(s) [attempted 360/8459 = 4%, 425 KB/s], Decompressed: 357
Downloaded: 398 file(s) [attempted 398/8459 = 4%, 616 KB/s], Decompressed: 395
Downloaded: 436 file(s) [attempted 436/8459 = 5%, 217 KB/s], Decompressed: 429
Downloaded: 470 file(s) [attempted 470/8459 = 5%, 711 KB/s], Decompressed: 460
Downloaded: 514 file(s) [attempted 514/8459 = 6%, 601 KB/s], Decompressed: 460
Downloaded: 552 file(s) [attempted 552/8459 = 6%, 287 KB/s], Decompressed: 463
Downloaded: 597 file(s) [attempted 597/8459 = 7%, 807 KB/s], Decompressed: 463
Downloaded: 638 file(s) [attempted 638/8459 = 7%, 859 KB/s], Decompressed: 545
Downloaded: 675 file(s) [attempted 675/8459 = 7%, 154 KB/s], Decompressed: 670
Downloaded: 710 file(s) [attempted 710/8459 = 8%, 1110 KB/s], Decompressed: 706
Downloaded: 754 file(s) [attempted 754/8459 = 8%, 296 KB/s], Decompressed: 747
Downloaded: 797 file(s) [attempted 797/8459 = 9%, 114 KB/s], Decompressed: 792
Downloaded: 836 file(s) [attempted 836/8459 = 9%, 317 KB/s], Decompressed: 833
Downloaded: 869 file(s) [attempted 869/8459 = 10%, 36 KB/s], Decompressed: 860
Downloaded: 905 file(s) [attempted 905/8459 = 10%, 349 KB/s], Decompressed: 902
Downloaded: 949 file(s) [attempted 949/8459 = 11%, 178 KB/s], Decompressed: 943
Downloaded: 994 file(s) [attempted 994/8459 = 11%, 154 KB/s], Decompressed: 991
Downloaded: 1038 file(s) [attempted 1038/8459 = 12%, 567 KB/s], Decompressed: 1035
Downloaded: 1076 file(s) [attempted 1076/8459 = 12%, 122 KB/s], Decompressed: 1069
Downloaded: 1111 file(s) [attempted 1111/8459 = 13%, 402 KB/s], Decompressed: 1107
Downloaded: 1151 file(s) [attempted 1151/8459 = 13%, 355 KB/s], Decompressed: 1148
Downloaded: 1193 file(s) [attempted 1193/8459 = 14%, 28 KB/s], Decompressed: 1189
Downloaded: 1234 file(s) [attempted 1234/8459 = 14%, 382 KB/s], Decompressed: 1223
Downloaded: 1270 file(s) [attempted 1270/8459 = 15%, 642 KB/s], Decompressed: 1261
Downloaded: 1309 file(s) [attempted 1309/8459 = 15%, 639 KB/s], Decompressed: 1302
Downloaded: 1347 file(s) [attempted 1347/8459 = 15%, 54 KB/s], Decompressed: 1340
Downloaded: 1388 file(s) [attempted 1388/8459 = 16%, 39 KB/s], Decompressed: 1360
Downloaded: 1425 file(s) [attempted 1425/8459 = 16%, 394 KB/s], Decompressed: 1360
Downloaded: 1466 file(s) [attempted 1466/8459 = 17%, 1712 KB/s], Decompressed: 1463
Downloaded: 1507 file(s) [attempted 1507/8459 = 17%, 792 KB/s], Decompressed: 1501
Downloaded: 1548 file(s) [attempted 1548/8459 = 18%, 350 KB/s], Decompressed: 1545
Downloaded: 1589 file(s) [attempted 1589/8459 = 18%, 308 KB/s], Decompressed: 1586
Downloaded: 1628 file(s) [attempted 1628/8459 = 19%, 684 KB/s], Decompressed: 1620
Downloaded: 1666 file(s) [attempted 1666/8459 = 19%, 299 KB/s], Decompressed: 1658
Downloaded: 1699 file(s) [attempted 1699/8459 = 20%, 119 KB/s], Decompressed: 1692
Downloaded: 1740 file(s) [attempted 1740/8459 = 20%, 191 KB/s], Decompressed: 1737
Downloaded: 1785 file(s) [attempted 1785/8459 = 21%, 281 KB/s], Decompressed: 1781
Downloaded: 1822 file(s) [attempted 1822/8459 = 21%, 624 KB/s], Decompressed: 1815
Downloaded: 1860 file(s) [attempted 1860/8459 = 21%, 381 KB/s], Decompressed: 1853
Downloaded: 1904 file(s) [attempted 1904/8459 = 22%, 77 KB/s], Decompressed: 1853
Downloaded: 1935 file(s) [attempted 1935/8459 = 22%, 340 KB/s], Decompressed: 1853
Downloaded: 1976 file(s) [attempted 1976/8459 = 23%, 48 KB/s], Decompressed: 1969
Downloaded: 2014 file(s) [attempted 2014/8459 = 23%, 61 KB/s], Decompressed: 2010
Downloaded: 2058 file(s) [attempted 2058/8459 = 24%, 90 KB/s], Decompressed: 2055
Downloaded: 2096 file(s) [attempted 2096/8459 = 24%, 295 KB/s], Decompressed: 2062
Downloaded: 2130 file(s) [attempted 2130/8459 = 25%, 569 KB/s], Decompressed: 2062
Downloaded: 2168 file(s) [attempted 2168/8459 = 25%, 271 KB/s], Decompressed: 2158
Downloaded: 2212 file(s) [attempted 2212/8459 = 26%, 286 KB/s], Decompressed: 2209
Downloaded: 2257 file(s) [attempted 2257/8459 = 26%, 69 KB/s], Decompressed: 2243
Downloaded: 2291 file(s) [attempted 2291/8459 = 27%, 133 KB/s], Decompressed: 2288
Downloaded: 2325 file(s) [attempted 2325/8459 = 27%, 477 KB/s], Decompressed: 2318
Downloaded: 2363 file(s) [attempted 2363/8459 = 27%, 1177 KB/s], Decompressed: 2360
Downloaded: 2407 file(s) [attempted 2407/8459 = 28%, 291 KB/s], Decompressed: 2404
Downloaded: 2450 file(s) [attempted 2450/8459 = 28%, 85 KB/s], Decompressed: 2442
Downloaded: 2488 file(s) [attempted 2488/8459 = 29%, 188 KB/s], Decompressed: 2479
Downloaded: 2517 file(s) [attempted 2517/8459 = 29%, 454 KB/s], Decompressed: 2514
Downloaded: 2561 file(s) [attempted 2561/8459 = 30%, 1268 KB/s], Decompressed: 2517
Downloaded: 2606 file(s) [attempted 2606/8459 = 30%, 134 KB/s], Decompressed: 2524
Downloaded: 2650 file(s) [attempted 2650/8459 = 31%, 257 KB/s], Decompressed: 2640
Downloaded: 2695 file(s) [attempted 2695/8459 = 31%, 186 KB/s], Decompressed: 2688
Downloaded: 2729 file(s) [attempted 2729/8459 = 32%, 73 KB/s], Decompressed: 2709
Downloaded: 2767 file(s) [attempted 2767/8459 = 32%, 342 KB/s], Decompressed: 2709
Downloaded: 2801 file(s) [attempted 2801/8459 = 33%, 219 KB/s], Decompressed: 2715
Downloaded: 2842 file(s) [attempted 2842/8459 = 33%, 325 KB/s], Decompressed: 2811
Downloaded: 2883 file(s) [attempted 2883/8459 = 34%, 184 KB/s], Decompressed: 2811
Downloaded: 2921 file(s) [attempted 2921/8459 = 34%, 613 KB/s], Decompressed: 2917
Downloaded: 2958 file(s) [attempted 2958/8459 = 34%, 1197 KB/s], Decompressed: 2924
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 187 KB/s], Decompressed: 2924
Downloaded: 3037 file(s) [attempted 3037/8459 = 35%, 18 KB/s], Decompressed: 3034
Downloaded: 3078 file(s) [attempted 3078/8459 = 36%, 903 KB/s], Decompressed: 3075
Downloaded: 3119 file(s) [attempted 3119/8459 = 36%, 157 KB/s], Decompressed: 3116
Downloaded: 3156 file(s) [attempted 3156/8459 = 37%, 183 KB/s], Decompressed: 3147
Downloaded: 3191 file(s) [attempted 3191/8459 = 37%, 179 KB/s], Decompressed: 3188
Downloaded: 3235 file(s) [attempted 3235/8459 = 38%, 110 KB/s], Decompressed: 3225
Downloaded: 3271 file(s) [attempted 3271/8459 = 38%, 216 KB/s], Decompressed: 3266
Downloaded: 3311 file(s) [attempted 3311/8459 = 39%, 1154 KB/s], Decompressed: 3304
Downloaded: 3345 file(s) [attempted 3345/8459 = 39%, 446 KB/s], Decompressed: 3342
Downloaded: 3386 file(s) [attempted 3386/8459 = 40%, 72 KB/s], Decompressed: 3379
Downloaded: 3427 file(s) [attempted 3427/8459 = 40%, 213 KB/s], Decompressed: 3379
Downloaded: 3465 file(s) [attempted 3465/8459 = 40%, 291 KB/s], Decompressed: 3379
Downloaded: 3499 file(s) [attempted 3499/8459 = 41%, 83 KB/s], Decompressed: 3386
Downloaded: 3540 file(s) [attempted 3540/8459 = 41%, 66 KB/s], Decompressed: 3386
Downloaded: 3578 file(s) [attempted 3578/8459 = 42%, 72 KB/s], Decompressed: 3386
Downloaded: 3622 file(s) [attempted 3622/8459 = 42%, 978 KB/s], Decompressed: 3468
Downloaded: 3667 file(s) [attempted 3667/8459 = 43%, 100 KB/s], Decompressed: 3656
Downloaded: 3701 file(s) [attempted 3701/8459 = 43%, 40 KB/s], Decompressed: 3656
Downloaded: 3739 file(s) [attempted 3739/8459 = 44%, 359 KB/s], Decompressed: 3656
Downloaded: 3776 file(s) [attempted 3776/8459 = 44%, 102 KB/s], Decompressed: 3667
Downloaded: 3821 file(s) [attempted 3821/8459 = 45%, 464 KB/s], Decompressed: 3667
Downloaded: 3862 file(s) [attempted 3862/8459 = 45%, 343 KB/s], Decompressed: 3746
Downloaded: 3893 file(s) [attempted 3893/8459 = 46%, 869 KB/s], Decompressed: 3746
Downloaded: 3934 file(s) [attempted 3934/8459 = 46%, 219 KB/s], Decompressed: 3920
Downloaded: 3971 file(s) [attempted 3971/8459 = 46%, 349 KB/s], Decompressed: 3968
Downloaded: 4013 file(s) [attempted 4013/8459 = 47%, 68 KB/s], Decompressed: 3985
Downloaded: 4057 file(s) [attempted 4057/8459 = 47%, 257 KB/s], Decompressed: 3985
Downloaded: 4095 file(s) [attempted 4095/8459 = 48%, 720 KB/s], Decompressed: 4088
Downloaded: 4132 file(s) [attempted 4132/8459 = 48%, 115 KB/s], Decompressed: 4125
Downloaded: 4170 file(s) [attempted 4170/8459 = 49%, 344 KB/s], Decompressed: 4163
Downloaded: 4204 file(s) [attempted 4204/8459 = 49%, 36 KB/s], Decompressed: 4163
Downloaded: 4245 file(s) [attempted 4245/8459 = 50%, 465 KB/s], Decompressed: 4163
Downloaded: 4286 file(s) [attempted 4286/8459 = 50%, 61 KB/s], Decompressed: 4280
Downloaded: 4324 file(s) [attempted 4324/8459 = 51%, 478 KB/s], Decompressed: 4321
Downloaded: 4365 file(s) [attempted 4365/8459 = 51%, 506 KB/s], Decompressed: 4348
Downloaded: 4399 file(s) [attempted 4399/8459 = 52%, 584 KB/s], Decompressed: 4348
Downloaded: 4437 file(s) [attempted 4437/8459 = 52%, 778 KB/s], Decompressed: 4358
Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 342 KB/s], Decompressed: 4358
Downloaded: 4516 file(s) [attempted 4516/8459 = 53%, 94 KB/s], Decompressed: 4358
Downloaded: 4557 file(s) [attempted 4557/8459 = 53%, 266 KB/s], Decompressed: 4437
Downloaded: 4588 file(s) [attempted 4588/8459 = 54%, 595 KB/s], Decompressed: 4437
Downloaded: 4629 file(s) [attempted 4629/8459 = 54%, 142 KB/s], Decompressed: 4437
Downloaded: 4664 file(s) [attempted 4664/8459 = 55%, 68 KB/s], Decompressed: 4659
Downloaded: 4700 file(s) [attempted 4700/8459 = 55%, 293 KB/s], Decompressed: 4694
Downloaded: 4742 file(s) [attempted 4742/8459 = 56%, 1169 KB/s], Decompressed: 4738
Downloaded: 4781 file(s) [attempted 4781/8459 = 56%, 142 KB/s], Decompressed: 4776
Downloaded: 4820 file(s) [attempted 4820/8459 = 56%, 218 KB/s], Decompressed: 4789
Downloaded: 4856 file(s) [attempted 4856/8459 = 57%, 72 KB/s], Decompressed: 4789
Downloaded: 4889 file(s) [attempted 4889/8459 = 57%, 421 KB/s], Decompressed: 4878
Downloaded: 4926 file(s) [attempted 4926/8459 = 58%, 427 KB/s], Decompressed: 4919
Downloaded: 4967 file(s) [attempted 4967/8459 = 58%, 122 KB/s], Decompressed: 4943
Downloaded: 5005 file(s) [attempted 5005/8459 = 59%, 307 KB/s], Decompressed: 4988
Downloaded: 5039 file(s) [attempted 5039/8459 = 59%, 257 KB/s], Decompressed: 4988
Downloaded: 5077 file(s) [attempted 5077/8459 = 60%, 311 KB/s], Decompressed: 4995
Downloaded: 5115 file(s) [attempted 5115/8459 = 60%, 1965 KB/s], Decompressed: 5111
Downloaded: 5156 file(s) [attempted 5156/8459 = 60%, 27 KB/s], Decompressed: 5142
Downloaded: 5190 file(s) [attempted 5190/8459 = 61%, 133 KB/s], Decompressed: 5183
Downloaded: 5228 file(s) [attempted 5228/8459 = 61%, 104 KB/s], Decompressed: 5217
Downloaded: 5269 file(s) [attempted 5269/8459 = 62%, 123 KB/s], Decompressed: 5217
Downloaded: 5310 file(s) [attempted 5310/8459 = 62%, 1083 KB/s], Decompressed: 5224
Downloaded: 5351 file(s) [attempted 5351/8459 = 63%, 140 KB/s], Decompressed: 5344
Downloaded: 5387 file(s) [attempted 5387/8459 = 63%, 764 KB/s], Decompressed: 5378
Downloaded: 5426 file(s) [attempted 5426/8459 = 64%, 289 KB/s], Decompressed: 5423
Downloaded: 5464 file(s) [attempted 5464/8459 = 64%, 134 KB/s], Decompressed: 5460
Downloaded: 5501 file(s) [attempted 5501/8459 = 65%, 964 KB/s], Decompressed: 5467
Downloaded: 5542 file(s) [attempted 5542/8459 = 65%, 219 KB/s], Decompressed: 5467
Downloaded: 5583 file(s) [attempted 5583/8459 = 66%, 344 KB/s], Decompressed: 5580
Downloaded: 5621 file(s) [attempted 5621/8459 = 66%, 191 KB/s], Decompressed: 5618
Downloaded: 5658 file(s) [attempted 5658/8459 = 66%, 137 KB/s], Decompressed: 5648
Downloaded: 5696 file(s) [attempted 5696/8459 = 67%, 111 KB/s], Decompressed: 5693
Downloaded: 5737 file(s) [attempted 5737/8459 = 67%, 259 KB/s], Decompressed: 5734
Downloaded: 5779 file(s) [attempted 5779/8459 = 68%, 61 KB/s], Decompressed: 5775
Downloaded: 5816 file(s) [attempted 5816/8459 = 68%, 219 KB/s], Decompressed: 5792
Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 621 KB/s], Decompressed: 5792
Downloaded: 5888 file(s) [attempted 5888/8459 = 69%, 288 KB/s], Decompressed: 5881
Downloaded: 5929 file(s) [attempted 5929/8459 = 70%, 104 KB/s], Decompressed: 5926
Downloaded: 5970 file(s) [attempted 5970/8459 = 70%, 222 KB/s], Decompressed: 5963
Downloaded: 6008 file(s) [attempted 6008/8459 = 71%, 480 KB/s], Decompressed: 6001
Downloaded: 6045 file(s) [attempted 6045/8459 = 71%, 66 KB/s], Decompressed: 6042
Downloaded: 6084 file(s) [attempted 6084/8459 = 71%, 315 KB/s], Decompressed: 6080
Downloaded: 6122 file(s) [attempted 6122/8459 = 72%, 88 KB/s], Decompressed: 6114
Downloaded: 6162 file(s) [attempted 6162/8459 = 72%, 869 KB/s], Decompressed: 6152
Downloaded: 6199 file(s) [attempted 6199/8459 = 73%, 57 KB/s], Decompressed: 6196
Downloaded: 6241 file(s) [attempted 6241/8459 = 73%, 50 KB/s], Decompressed: 6199
Downloaded: 6278 file(s) [attempted 6278/8459 = 74%, 188 KB/s], Decompressed: 6199
Downloaded: 6316 file(s) [attempted 6316/8459 = 74%, 403 KB/s], Decompressed: 6302
Downloaded: 6351 file(s) [attempted 6351/8459 = 75%, 101 KB/s], Decompressed: 6347
Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 65 KB/s], Decompressed: 6384
Downloaded: 6429 file(s) [attempted 6429/8459 = 76%, 313 KB/s], Decompressed: 6391
Downloaded: 6466 file(s) [attempted 6466/8459 = 76%, 132 KB/s], Decompressed: 6391
Downloaded: 6507 file(s) [attempted 6507/8459 = 76%, 419 KB/s], Decompressed: 6501
Downloaded: 6545 file(s) [attempted 6545/8459 = 77%, 326 KB/s], Decompressed: 6538
Downloaded: 6583 file(s) [attempted 6583/8459 = 77%, 338 KB/s], Decompressed: 6579
Downloaded: 6624 file(s) [attempted 6624/8459 = 78%, 232 KB/s], Decompressed: 6620
Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 194 KB/s], Decompressed: 6661
Downloaded: 6699 file(s) [attempted 6699/8459 = 79%, 108 KB/s], Decompressed: 6696
Downloaded: 6740 file(s) [attempted 6740/8459 = 79%, 745 KB/s], Decompressed: 6733
Downloaded: 6776 file(s) [attempted 6776/8459 = 80%, 976 KB/s], Decompressed: 6768
Downloaded: 6815 file(s) [attempted 6815/8459 = 80%, 171 KB/s], Decompressed: 6781
Downloaded: 6857 file(s) [attempted 6857/8459 = 81%, 403 KB/s], Decompressed: 6788
Downloaded: 6894 file(s) [attempted 6894/8459 = 81%, 190 KB/s], Decompressed: 6822
Downloaded: 6939 file(s) [attempted 6939/8459 = 82%, 284 KB/s], Decompressed: 6935
Downloaded: 6976 file(s) [attempted 6976/8459 = 82%, 537 KB/s], Decompressed: 6970
Downloaded: 7016 file(s) [attempted 7016/8459 = 82%, 262 KB/s], Decompressed: 7007
Downloaded: 7052 file(s) [attempted 7052/8459 = 83%, 238 KB/s], Decompressed: 7045
Downloaded: 7089 file(s) [attempted 7089/8459 = 83%, 1145 KB/s], Decompressed: 7086
Downloaded: 7130 file(s) [attempted 7130/8459 = 84%, 279 KB/s], Decompressed: 7127
Downloaded: 7171 file(s) [attempted 7171/8459 = 84%, 142 KB/s], Decompressed: 7168
Downloaded: 7206 file(s) [attempted 7206/8459 = 85%, 255 KB/s], Decompressed: 7195
Downloaded: 7243 file(s) [attempted 7243/8459 = 85%, 712 KB/s], Decompressed: 7219
Downloaded: 7284 file(s) [attempted 7284/8459 = 86%, 45 KB/s], Decompressed: 7219
Downloaded: 7329 file(s) [attempted 7329/8459 = 86%, 161 KB/s], Decompressed: 7325
Downloaded: 7373 file(s) [attempted 7373/8459 = 87%, 93 KB/s], Decompressed: 7353
Downloaded: 7408 file(s) [attempted 7408/8459 = 87%, 82 KB/s], Decompressed: 7353
Downloaded: 7445 file(s) [attempted 7445/8459 = 88%, 62 KB/s], Decompressed: 7353
Downloaded: 7486 file(s) [attempted 7486/8459 = 88%, 164 KB/s], Decompressed: 7353
Downloaded: 7524 file(s) [attempted 7524/8459 = 88%, 176 KB/s], Decompressed: 7353
Downloaded: 7565 file(s) [attempted 7565/8459 = 89%, 269 KB/s], Decompressed: 7353
Downloaded: 7596 file(s) [attempted 7596/8459 = 89%, 452 KB/s], Decompressed: 7360
Downloaded: 7637 file(s) [attempted 7637/8459 = 90%, 69 KB/s], Decompressed: 7623
Downloaded: 7678 file(s) [attempted 7678/8459 = 90%, 129 KB/s], Decompressed: 7623
Downloaded: 7716 file(s) [attempted 7716/8459 = 91%, 43 KB/s], Decompressed: 7630
Downloaded: 7757 file(s) [attempted 7757/8459 = 91%, 338 KB/s], Decompressed: 7630
Downloaded: 7787 file(s) [attempted 7787/8459 = 92%, 319 KB/s], Decompressed: 7630
Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 1867 KB/s], Decompressed: 7709
Downloaded: 7866 file(s) [attempted 7866/8459 = 92%, 231 KB/s], Decompressed: 7709
Downloaded: 7904 file(s) [attempted 7904/8459 = 93%, 782 KB/s], Decompressed: 7876
Downloaded: 7941 file(s) [attempted 7941/8459 = 93%, 233 KB/s], Decompressed: 7876
Downloaded: 7979 file(s) [attempted 7979/8459 = 94%, 297 KB/s], Decompressed: 7965
Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 136 KB/s], Decompressed: 8010
Downloaded: 8058 file(s) [attempted 8058/8459 = 95%, 684 KB/s], Decompressed: 8051
Downloaded: 8099 file(s) [attempted 8099/8459 = 95%, 71 KB/s], Decompressed: 8089
Downloaded: 8133 file(s) [attempted 8133/8459 = 96%, 311 KB/s], Decompressed: 8126
Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 124 KB/s], Decompressed: 8167
Downloaded: 8212 file(s) [attempted 8212/8459 = 97%, 422 KB/s], Decompressed: 8174
Downloaded: 8253 file(s) [attempted 8253/8459 = 97%, 51 KB/s], Decompressed: 8174
Downloaded: 8287 file(s) [attempted 8287/8459 = 97%, 117 KB/s], Decompressed: 8277
Downloaded: 8325 file(s) [attempted 8325/8459 = 98%, 326 KB/s], Decompressed: 8321
Downloaded: 8366 file(s) [attempted 8366/8459 = 98%, 724 KB/s], Decompressed: 8362
Downloaded: 8410 file(s) [attempted 8410/8459 = 99%, 106 KB/s], Decompressed: 8407
Downloaded: 8451 file(s) [attempted 8451/8459 = 99%, 469 KB/s], Decompressed: 8441
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 469 KB/s], Decompressed: 8452

lake build

ℹ [3537/3549] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3559/3576] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
⚠ [3694/3710] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3811/3818] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3817/3824] Built PrimeNumberTheoremAnd.IEANTN.Mertens (191s)
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:922:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:935:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:948:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:961:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:973:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1039:8: declaration uses `sorry`
⚠ [3880/3892] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (51s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2577:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2578:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2599:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2600:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2817:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2818:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2833:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2834:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2963:4: `simp [W]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2964:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3069:4: `simp [p]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3070:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: `simp [Set.uIcc_of_le hab]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: Try this:
  [apply] simp only [_root_.deriv_ofReal]
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3085:4: `fun_prop` uses `⊢`!
⚠ [3881/3892] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [3883/3893] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (3.2s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
✔ [3887/3895] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (2.5s)
✔ [3890/3895] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (11s)
⚠ [3891/3895] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (5.5s)
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
✔ [3894/3903] Built PrimeNumberTheoremAnd.IEANTN.CostaPereira (8.7s)
⚠ [4014/4022] Built PrimeNumberTheoremAnd.IEANTN.Buthe (11s)
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
⚠ [4018/4025] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (21s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
⚠ [4020/4026] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (11s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4022/4036] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (27s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
✔ [4033/4061] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (5.0s)
✔ [4036/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core (7.7s)
✔ [4038/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85 (17s)
✔ [4039/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc (11s)
✔ [4040/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000 (65s)
✔ [4041/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500 (40s)
✔ [4042/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500 (39s)
✔ [4043/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500 (39s)
✔ [4044/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500 (40s)
✔ [4045/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875 (39s)
✔ [4046/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375 (40s)
✔ [4047/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875 (39s)
✔ [4048/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375 (39s)
✔ [4049/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875 (39s)
✔ [4050/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375 (40s)
✔ [4051/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875 (39s)
✔ [4052/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95 (5.4s)
✔ [4053/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values (9.7s)
✔ [4054/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next (18s)
ℹ [4055/4068] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (46s)
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
✔ [4057/4070] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (3.8s)
✔ [4059/4072] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43 (61s)
⚠ [4060/4072] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (12s)
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3245:4: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3572:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3819:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3847:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3859:8: declaration uses `sorry`
⚠ [4062/4074] Replayed PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
✔ [4064/4074] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59 (40s)
✔ [4066/4074] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (14s)
⚠ [4067/4074] Built PrimeNumberTheoremAnd.IEANTN.Dusart (17s)
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:736:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:748:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:760:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:772:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:784:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:808:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:820:8: declaration uses `sorry`
✔ [4070/4074] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows (5.9s)
⚠ [4072/4074] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (57s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:316:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3781:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3784:6: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3786:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: The following tactic starts with 2 goals and ends with 2 goals, 1 of which is not operated on.
  ring
Please focus on the current goal, for instance using `·` (typed as "\.").

Note: This linter can be disabled with `set_option linter.style.multiGoal false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3827:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3830:8: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3836:4: `have h63 :=
  theorem_6_3 (by linarith : 14 ≤ x₁) x₂.toReal
    (by
      cases x₂ <;> norm_num at *; · linarith;
      · exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
    x hx₁
    (by
      cases x₂ <;> norm_num at *; · linarith;
      · exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
    (by
      cases x₂ <;> norm_num at *; · exact_mod_cast hc;
      · exact mul_nonneg (by linarith) (Real.log_nonneg (by linarith)))` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3846:4: `unfold μ_num_1` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: `simp_all +decide [ mul_assoc, mul_comm, mul_left_comm ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: Try this:
  [apply] simp_all +decide only [Fin.Iio_last_eq_map, Finset.sum_sub_distrib, Finset.sum_map, Fin.coe_castSuccEmb,
    Fin.coeSucc_eq_succ, ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3849:6: `exact absurd (this y hy₁) (by norm_num [h]; linarith)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3858:6: `exact absurd ‹_› (not_le_of_gt hc)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4652:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4674:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4701:8: declaration uses `sorry`
✔ [4073/4103] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch (17s)
✔ [4087/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore (17s)
✔ [4091/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13 (13s)
✔ [4092/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12 (21s)
✔ [4093/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11 (21s)
✔ [4094/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10 (21s)
✔ [4095/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09 (22s)
✔ [4096/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08 (21s)
✔ [4097/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07 (21s)
✔ [4098/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06 (21s)
✔ [4099/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05 (21s)
✔ [4100/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04 (21s)
✔ [4101/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03 (21s)
✔ [4102/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02 (21s)
✔ [4103/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01 (21s)
✔ [4104/4111] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00 (21s)
⚠ [4108/4111] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext (4.0s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4110/4116] Built PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor (6.7s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:19:72: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:109:37: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:122:60: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:203:39: missing space in the source

This part of the code
  '(3/2) 0.8476'
should be written as
  '(3 / 2)'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
⚠ [4120/4130] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4125/4164] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (9.3s)
⚠ [4144/4181] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (13s)
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:62:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:84:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:100:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:141:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:287:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:295:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:424:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:469:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:484:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:527:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:536:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:545:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:579:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:588:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:597:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:632:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:641:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:650:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:676:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:710:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:721:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:732:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:750:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:759:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:768:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:891:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:911:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:941:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:967:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:981:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:989:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1004:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1019:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1028:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1043:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1061:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1073:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1101:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1123:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1137:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1151:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1181:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1232:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1246:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1260:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1288:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1323:8: declaration uses `sorry`
⚠ [4152/4187] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (9.4s)
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:60:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:203:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:213:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:255:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:337:8: declaration uses `sorry`
✔ [4154/4187] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.DigammaSeries (17s)
ℹ [4157/4187] Replayed PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations
info: PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:76:4: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
⚠ [4158/4187] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline

Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
✔ [4163/4187] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (11s)
⚠ [4166/4187] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (6.3s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4169/4187] Built PrimeNumberTheoremAnd.IEANTN.Lcm (26s)
✔ [4170/4187] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (53s)
✔ [4175/4187] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (2.6s)
⚠ [4185/4187] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (13s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:132:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:206:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:325:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:357:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1490:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2720:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2746:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3352:8: declaration uses `sorry`
✔ [4186/4187] Built PrimeNumberTheoremAnd (3.1s)
Build completed successfully (4187 jobs).

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

lake build :blueprint

✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (1.8s)
✔ [25/35] Built Cli.Basic:c.o (3.1s)
✔ [32/35] Built Cli.Extensions:c.o (502ms)
✔ [33/35] Built Cli:c.o (66ms)
ℹ [3595/3612] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3623/3643] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
⚠ [3767/3788] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3885/3900] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3894/3901] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:922:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:935:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:948:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:961:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:973:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1039:8: declaration uses `sorry`
✔ [3900/3916] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (49s)
⚠ [3964/3986] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2577:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2578:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2599:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2600:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2817:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2818:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2833:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2834:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2963:4: `simp [W]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2964:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3069:4: `simp [p]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3070:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: `simp [Set.uIcc_of_le hab]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: Try this:
  [apply] simp only [_root_.deriv_ofReal]
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3085:4: `fun_prop` uses `⊢`!
⚠ [3965/3986] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [3967/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (26s)
⚠ [3968/3988] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaSummary
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
✔ [3974/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaSummary:blueprint (3.3s)
✔ [3981/3990] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (2.9s)
⚠ [3982/3990] Replayed PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
✔ [3984/3992] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (16s)
✔ [3985/3992] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (9.6s)
✔ [3988/4000] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CostaPereira:blueprint (6.8s)
⚠ [4107/4122] Replayed PrimeNumberTheoremAnd.IEANTN.Buthe
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
⚠ [4111/4126] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
✔ [4114/4126] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (6.3s)
⚠ [4115/4126] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
✔ [4119/4130] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (18s)
✔ [4120/4177] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (21s)
⚠ [4122/4177] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
✔ [4125/4186] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (24s)
✔ [4136/4198] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (4.8s)
✔ [4139/4200] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core:blueprint (2.0s)
ℹ [4153/4200] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
✔ [4161/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next:blueprint (2.0s)
✔ [4162/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values:blueprint (2.0s)
✔ [4164/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85:blueprint (3.1s)
✔ [4165/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95:blueprint (2.0s)
✔ [4166/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875:blueprint (3.0s)
✔ [4167/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375:blueprint (3.1s)
✔ [4168/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875:blueprint (3.0s)
✔ [4169/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375:blueprint (2.0s)
✔ [4170/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875:blueprint (2.0s)
✔ [4171/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375:blueprint (3.0s)
✔ [4172/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875:blueprint (3.0s)
✔ [4173/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500:blueprint (3.1s)
✔ [4174/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500:blueprint (3.1s)
✔ [4175/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500:blueprint (3.0s)
✔ [4176/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500:blueprint (3.0s)
✔ [4177/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000:blueprint (2.0s)
✔ [4178/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc:blueprint (2.0s)
✔ [4179/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (50s)
⚠ [4180/4206] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3245:4: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3572:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3819:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3847:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3859:8: declaration uses `sorry`
✔ [4182/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (4.5s)
⚠ [4184/4206] Replayed PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
✔ [4187/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43:blueprint (3.2s)
✔ [4189/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (19s)
⚠ [4192/4206] Replayed PrimeNumberTheoremAnd.IEANTN.Dusart
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:736:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:748:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:760:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:772:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:784:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:808:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:820:8: declaration uses `sorry`
✔ [4195/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (18s)
✔ [4196/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (19s)
✔ [4197/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59:blueprint (2.0s)
⚠ [4200/4206] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:316:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3781:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3784:6: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3786:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: The following tactic starts with 2 goals and ends with 2 goals, 1 of which is not operated on.
  ring
Please focus on the current goal, for instance using `·` (typed as "\.").

Note: This linter can be disabled with `set_option linter.style.multiGoal false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3827:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3830:8: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3836:4: `have h63 :=
  theorem_6_3 (by linarith : 14 ≤ x₁) x₂.toReal
    (by
      cases x₂ <;> norm_num at *; · linarith;
      · exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
    x hx₁
    (by
      cases x₂ <;> norm_num at *; · linarith;
      · exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
    (by
      cases x₂ <;> norm_num at *; · exact_mod_cast hc;
      · exact mul_nonneg (by linarith) (Real.log_nonneg (by linarith)))` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3846:4: `unfold μ_num_1` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: `simp_all +decide [ mul_assoc, mul_comm, mul_left_comm ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: Try this:
  [apply] simp_all +decide only [Fin.Iio_last_eq_map, Finset.sum_sub_distrib, Finset.sum_map, Fin.coe_castSuccEmb,
    Fin.coeSucc_eq_succ, ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3849:6: `exact absurd (this y hy₁) (by norm_num [h]; linarith)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3858:6: `exact absurd ‹_› (not_le_of_gt hc)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4652:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4674:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4701:8: declaration uses `sorry`
✔ [4201/4212] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows:blueprint (2.9s)
✔ [4204/4212] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (32s)
✔ [4206/4251] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch:blueprint (16s)
✔ [4226/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore:blueprint (3.1s)
✔ [4242/4263] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00:blueprint (2.0s)
✔ [4243/4263] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01:blueprint (2.0s)
✔ [4244/4263] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02:blueprint (2.0s)
✔ [4245/4263] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03:blueprint (3.0s)
✔ [4246/4263] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04:blueprint (3.0s)
✔ [4247/4263] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05:blueprint (3.0s)
✔ [4248/4263] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06:blueprint (2.0s)
✔ [4249/4263] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07:blueprint (3.0s)
✔ [4250/4263] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08:blueprint (2.0s)
✔ [4251/4263] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09:blueprint (2.9s)
✔ [4252/4263] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10:blueprint (2.0s)
✔ [4253/4263] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11:blueprint (3.0s)
✔ [4254/4263] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12:blueprint (2.9s)
✔ [4255/4263] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13:blueprint (3.1s)
⚠ [4256/4263] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
✔ [4259/4267] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext:blueprint (2.0s)
⚠ [4260/4267] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:19:72: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:109:37: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:122:60: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:203:39: missing space in the source

This part of the code
  '(3/2) 0.8476'
should be written as
  '(3 / 2)'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
✔ [4263/4353] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor:blueprint (3.0s)
⚠ [4273/4353] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4279/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (3.0s)
⚠ [4280/4356] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:62:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:84:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:100:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:141:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:287:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:295:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:424:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:469:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:484:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:527:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:536:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:545:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:579:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:588:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:597:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:632:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:641:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:650:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:676:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:710:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:721:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:732:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:750:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:759:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:768:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:891:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:911:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:941:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:967:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:981:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:989:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1004:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1019:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1028:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1043:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1061:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1073:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1101:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1123:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1137:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1151:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1181:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1232:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1246:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1260:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1288:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1323:8: declaration uses `sorry`
✔ [4299/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (45s)
⚠ [4300/4395] Replayed PrimeNumberTheoremAnd.IEANTN.SecondarySummary
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:60:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:203:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:213:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:255:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:337:8: declaration uses `sorry`
ℹ [4328/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations
info: PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:76:4: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
⚠ [4329/4395] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline

Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
✔ [4336/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (6.5s)
⚠ [4337/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4344/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.DigammaSeries:blueprint (2.4s)
✔ [4354/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (10s)
✔ [4356/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (5.0s)
✔ [4367/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (10s)
✔ [4368/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (2.9s)
✔ [4369/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (15s)
⚠ [4390/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:132:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:206:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:325:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:357:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1490:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2720:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2746:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3352:8: declaration uses `sorry`
✔ [4391/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (43s)
✔ [4393/4396] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (3.2s)
ℹ [4394/4396] Replayed PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint
info: Blueprint indexing
Build completed successfully (4396 jobs).

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-a)

apx-semantic-phase	{"duration_ms":22,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":452,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_00.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":437878,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_00.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_00.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":74842,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":74842,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":433,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_01.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":421991,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_01.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_01.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":77992,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":77992,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":370,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_02.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":452434,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_02.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_02.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":80054,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":80054,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":405,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_03.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":433565,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_03.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_03.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":82759,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":82759,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":445,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_04.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":425173,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_04.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_04.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":85603,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":85603,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":341,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_13.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":423423,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_13.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_13.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":5,"module_payload_kind":"fragment","ok":true,"payload_bytes":68407,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":5,"module_payload_kind":"fragment","ok":true,"payload_bytes":68407,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":9689,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 636a28aae52bd7764b1dadb4c26fae58852a4ce15fa88c89f2ae6794133dfe50
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":49,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":2667603,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-b)

apx-semantic-phase	{"duration_ms":38,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":489,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_05.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":447476,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_05.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_05.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":87967,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":87967,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":393,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_06.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":448197,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_06.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_06.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":90257,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":90257,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":425,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_07.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":437165,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_07.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_07.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":92539,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":92539,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":400,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_08.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":436112,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_08.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_08.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":94376,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":94376,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":383,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_09.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":433512,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_09.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_09.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":96327,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":96327,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":24}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":11925,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 636a28aae52bd7764b1dadb4c26fae58852a4ce15fa88c89f2ae6794133dfe50
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":51,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":2228555,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r2)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":424,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_10.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":435167,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_10.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_10.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":101240,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":101240,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":388,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_11.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":434599,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_11.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_11.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":102723,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":102723,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":498,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_12.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":432833,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_12.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_12.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":107456,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":107456,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":136,"diagnostic_count":71,"duration_ms":10867,"module_name":"PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky","module_path":"PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":417916,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky","module_path":"PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":136,"diagnostic_count":71,"duration_ms":5,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky","module_path":"PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":509503,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":509503,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":41,"diagnostic_count":6,"duration_ms":2953,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":437346,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":41,"diagnostic_count":6,"duration_ms":2,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":344830,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":344830,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":297,"diagnostic_count":259,"duration_ms":23200,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":438230,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":297,"diagnostic_count":259,"duration_ms":32,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":5,"module_payload_kind":"fragment","ok":true,"payload_bytes":1556361,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":5,"module_payload_kind":"fragment","ok":true,"payload_bytes":1556361,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":21}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":9698,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 636a28aae52bd7764b1dadb4c26fae58852a4ce15fa88c89f2ae6794133dfe50
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":33,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":2640268,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r3)

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":194,"diagnostic_count":65,"duration_ms":23052,"module_name":"PrimeNumberTheoremAnd.IEANTN.Kadiri","module_path":"PrimeNumberTheoremAnd/IEANTN/Kadiri.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":410186,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Kadiri","module_path":"PrimeNumberTheoremAnd/IEANTN/Kadiri.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":194,"diagnostic_count":65,"duration_ms":14,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Kadiri","module_path":"PrimeNumberTheoremAnd/IEANTN/Kadiri.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":2589283,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":2589283,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":8,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimarySummary.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":420061,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimarySummary.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimarySummary.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":502,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":502,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":255,"diagnostic_count":136,"duration_ms":20772,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":431749,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":255,"diagnostic_count":136,"duration_ms":25,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1265099,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1265099,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":10}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":10481,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 636a28aae52bd7764b1dadb4c26fae58852a4ce15fa88c89f2ae6794133dfe50
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":44,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1310768,"ok":true}

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r4)

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":70,"diagnostic_count":54,"duration_ms":4995,"module_name":"PrimeNumberTheoremAnd.IEANTN.Goldbach","module_path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":432503,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Goldbach","module_path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":70,"diagnostic_count":54,"duration_ms":3,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Goldbach","module_path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":396745,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":3,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":396745,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":235,"diagnostic_count":164,"duration_ms":18209,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":434451,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":235,"diagnostic_count":164,"duration_ms":24,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1491369,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1491369,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":263,"diagnostic_count":178,"duration_ms":22605,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":431323,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":263,"diagnostic_count":178,"duration_ms":26,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1806664,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1806664,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":67,"diagnostic_count":53,"duration_ms":5223,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":443115,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":67,"diagnostic_count":53,"duration_ms":5,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":257157,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":257157,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":17}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":9564,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 636a28aae52bd7764b1dadb4c26fae58852a4ce15fa88c89f2ae6794133dfe50
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":21,"runner_cache_hit":true}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":1800334,"ok":true}