Run 58

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

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

git checkout 1fad44dd5817c5aebe0a19c23b2927839429288e

Note: switching to '1fad44dd5817c5aebe0a19c23b2927839429288e'.

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 1fad44d feat(laplace): add PR1 inversion foundation (#1573)

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%, 9 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 1 KB/s], Decompressed: 13
Downloaded: 41 file(s) [attempted 41/8459 = 0%, 16 KB/s], Decompressed: 37
Downloaded: 68 file(s) [attempted 68/8459 = 0%, 26 KB/s], Decompressed: 65
Downloaded: 93 file(s) [attempted 93/8459 = 1%, 501 KB/s], Decompressed: 90
Downloaded: 128 file(s) [attempted 128/8459 = 1%, 241 KB/s], Decompressed: 124
Downloaded: 165 file(s) [attempted 165/8459 = 1%, 489 KB/s], Decompressed: 162
Downloaded: 203 file(s) [attempted 203/8459 = 2%, 31 KB/s], Decompressed: 199
Downloaded: 237 file(s) [attempted 237/8459 = 2%, 432 KB/s], Decompressed: 223
Downloaded: 275 file(s) [attempted 275/8459 = 3%, 794 KB/s], Decompressed: 271
Downloaded: 316 file(s) [attempted 316/8459 = 3%, 327 KB/s], Decompressed: 306
Downloaded: 357 file(s) [attempted 357/8459 = 4%, 952 KB/s], Decompressed: 353
Downloaded: 398 file(s) [attempted 398/8459 = 4%, 1324 KB/s], Decompressed: 391
Downloaded: 432 file(s) [attempted 432/8459 = 5%, 28 KB/s], Decompressed: 422
Downloaded: 466 file(s) [attempted 466/8459 = 5%, 156 KB/s], Decompressed: 460
Downloaded: 508 file(s) [attempted 508/8459 = 6%, 772 KB/s], Decompressed: 504
Downloaded: 552 file(s) [attempted 552/8459 = 6%, 282 KB/s], Decompressed: 549
Downloaded: 600 file(s) [attempted 600/8459 = 7%, 35 KB/s], Decompressed: 597
Downloaded: 641 file(s) [attempted 641/8459 = 7%, 243 KB/s], Decompressed: 634
Downloaded: 673 file(s) [attempted 673/8459 = 7%, 236 KB/s], Decompressed: 665
Downloaded: 713 file(s) [attempted 713/8459 = 8%, 185 KB/s], Decompressed: 710
Downloaded: 754 file(s) [attempted 754/8459 = 8%, 121 KB/s], Decompressed: 751
Downloaded: 801 file(s) [attempted 801/8459 = 9%, 712 KB/s], Decompressed: 792
Downloaded: 840 file(s) [attempted 840/8459 = 9%, 171 KB/s], Decompressed: 833
Downloaded: 871 file(s) [attempted 871/8459 = 10%, 363 KB/s], Decompressed: 864
Downloaded: 912 file(s) [attempted 912/8459 = 10%, 299 KB/s], Decompressed: 905
Downloaded: 956 file(s) [attempted 956/8459 = 11%, 156 KB/s], Decompressed: 953
Downloaded: 997 file(s) [attempted 997/8459 = 11%, 267 KB/s], Decompressed: 994
Downloaded: 1042 file(s) [attempted 1042/8459 = 12%, 583 KB/s], Decompressed: 1032
Downloaded: 1073 file(s) [attempted 1073/8459 = 12%, 92 KB/s], Decompressed: 1066
Downloaded: 1110 file(s) [attempted 1110/8459 = 13%, 214 KB/s], Decompressed: 1107
Downloaded: 1151 file(s) [attempted 1151/8459 = 13%, 105 KB/s], Decompressed: 1148
Downloaded: 1196 file(s) [attempted 1196/8459 = 14%, 27 KB/s], Decompressed: 1186
Downloaded: 1230 file(s) [attempted 1230/8459 = 14%, 86 KB/s], Decompressed: 1227
Downloaded: 1271 file(s) [attempted 1271/8459 = 15%, 1483 KB/s], Decompressed: 1264
Downloaded: 1311 file(s) [attempted 1311/8459 = 15%, 256 KB/s], Decompressed: 1305
Downloaded: 1350 file(s) [attempted 1350/8459 = 15%, 51 KB/s], Decompressed: 1346
Downloaded: 1391 file(s) [attempted 1391/8459 = 16%, 378 KB/s], Decompressed: 1388
Downloaded: 1429 file(s) [attempted 1429/8459 = 16%, 28 KB/s], Decompressed: 1425
Downloaded: 1466 file(s) [attempted 1466/8459 = 17%, 180 KB/s], Decompressed: 1456
Downloaded: 1507 file(s) [attempted 1507/8459 = 17%, 53 KB/s], Decompressed: 1500
Downloaded: 1548 file(s) [attempted 1548/8459 = 18%, 203 KB/s], Decompressed: 1545
Downloaded: 1589 file(s) [attempted 1589/8459 = 18%, 317 KB/s], Decompressed: 1583
Downloaded: 1627 file(s) [attempted 1627/8459 = 19%, 1609 KB/s], Decompressed: 1620
Downloaded: 1665 file(s) [attempted 1665/8459 = 19%, 1657 KB/s], Decompressed: 1658
Downloaded: 1702 file(s) [attempted 1702/8459 = 20%, 117 KB/s], Decompressed: 1696
Downloaded: 1744 file(s) [attempted 1744/8459 = 20%, 232 KB/s], Decompressed: 1737
Downloaded: 1781 file(s) [attempted 1781/8459 = 21%, 184 KB/s], Decompressed: 1774
Downloaded: 1819 file(s) [attempted 1819/8459 = 21%, 212 KB/s], Decompressed: 1815
Downloaded: 1860 file(s) [attempted 1860/8459 = 21%, 378 KB/s], Decompressed: 1856
Downloaded: 1897 file(s) [attempted 1897/8459 = 22%, 43 KB/s], Decompressed: 1894
Downloaded: 1942 file(s) [attempted 1942/8459 = 22%, 428 KB/s], Decompressed: 1939
Downloaded: 1980 file(s) [attempted 1980/8459 = 23%, 480 KB/s], Decompressed: 1973
Downloaded: 2014 file(s) [attempted 2014/8459 = 23%, 50 KB/s], Decompressed: 2007
Downloaded: 2058 file(s) [attempted 2058/8459 = 24%, 37 KB/s], Decompressed: 2052
Downloaded: 2099 file(s) [attempted 2099/8459 = 24%, 297 KB/s], Decompressed: 2096
Downloaded: 2141 file(s) [attempted 2141/8459 = 25%, 502 KB/s], Decompressed: 2134
Downloaded: 2175 file(s) [attempted 2175/8459 = 25%, 198 KB/s], Decompressed: 2168
Downloaded: 2216 file(s) [attempted 2216/8459 = 26%, 177 KB/s], Decompressed: 2209
Downloaded: 2253 file(s) [attempted 2253/8459 = 26%, 1146 KB/s], Decompressed: 2250
Downloaded: 2295 file(s) [attempted 2295/8459 = 27%, 953 KB/s], Decompressed: 2291
Downloaded: 2336 file(s) [attempted 2336/8459 = 27%, 276 KB/s], Decompressed: 2325
Downloaded: 2373 file(s) [attempted 2373/8459 = 28%, 747 KB/s], Decompressed: 2370
Downloaded: 2407 file(s) [attempted 2407/8459 = 28%, 125 KB/s], Decompressed: 2404
Downloaded: 2452 file(s) [attempted 2452/8459 = 28%, 90 KB/s], Decompressed: 2448
Downloaded: 2493 file(s) [attempted 2493/8459 = 29%, 78 KB/s], Decompressed: 2490
Downloaded: 2534 file(s) [attempted 2534/8459 = 29%, 583 KB/s], Decompressed: 2531
Downloaded: 2572 file(s) [attempted 2572/8459 = 30%, 161 KB/s], Decompressed: 2568
Downloaded: 2606 file(s) [attempted 2606/8459 = 30%, 556 KB/s], Decompressed: 2603
Downloaded: 2653 file(s) [attempted 2653/8459 = 31%, 320 KB/s], Decompressed: 2647
Downloaded: 2690 file(s) [attempted 2690/8459 = 31%, 785 KB/s], Decompressed: 2681
Downloaded: 2729 file(s) [attempted 2729/8459 = 32%, 75 KB/s], Decompressed: 2726
Downloaded: 2767 file(s) [attempted 2767/8459 = 32%, 54 KB/s], Decompressed: 2763
Downloaded: 2804 file(s) [attempted 2804/8459 = 33%, 465 KB/s], Decompressed: 2801
Downloaded: 2849 file(s) [attempted 2849/8459 = 33%, 1397 KB/s], Decompressed: 2842
Downloaded: 2887 file(s) [attempted 2887/8459 = 34%, 309 KB/s], Decompressed: 2876
Downloaded: 2928 file(s) [attempted 2928/8459 = 34%, 763 KB/s], Decompressed: 2923
Downloaded: 2965 file(s) [attempted 2965/8459 = 35%, 420 KB/s], Decompressed: 2958
Downloaded: 3003 file(s) [attempted 3003/8459 = 35%, 908 KB/s], Decompressed: 3000
Downloaded: 3044 file(s) [attempted 3044/8459 = 35%, 159 KB/s], Decompressed: 3037
Downloaded: 3088 file(s) [attempted 3088/8459 = 36%, 222 KB/s], Decompressed: 3085
Downloaded: 3133 file(s) [attempted 3133/8459 = 37%, 101 KB/s], Decompressed: 3119
Downloaded: 3171 file(s) [attempted 3171/8459 = 37%, 634 KB/s], Decompressed: 3167
Downloaded: 3208 file(s) [attempted 3208/8459 = 37%, 508 KB/s], Decompressed: 3205
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 228 KB/s], Decompressed: 3246
Downloaded: 3288 file(s) [attempted 3288/8459 = 38%, 93 KB/s], Decompressed: 3284
Downloaded: 3335 file(s) [attempted 3335/8459 = 39%, 145 KB/s], Decompressed: 3328
Downloaded: 3377 file(s) [attempted 3377/8459 = 39%, 639 KB/s], Decompressed: 3366
Downloaded: 3414 file(s) [attempted 3414/8459 = 40%, 352 KB/s], Decompressed: 3410
Downloaded: 3455 file(s) [attempted 3455/8459 = 40%, 458 KB/s], Decompressed: 3451
Downloaded: 3492 file(s) [attempted 3492/8459 = 41%, 377 KB/s], Decompressed: 3485
Downloaded: 3533 file(s) [attempted 3533/8459 = 41%, 137 KB/s], Decompressed: 3530
Downloaded: 3578 file(s) [attempted 3578/8459 = 42%, 80 KB/s], Decompressed: 3571
Downloaded: 3616 file(s) [attempted 3616/8459 = 42%, 550 KB/s], Decompressed: 3612
Downloaded: 3653 file(s) [attempted 3653/8459 = 43%, 593 KB/s], Decompressed: 3650
Downloaded: 3694 file(s) [attempted 3694/8459 = 43%, 243 KB/s], Decompressed: 3687
Downloaded: 3735 file(s) [attempted 3735/8459 = 44%, 268 KB/s], Decompressed: 3725
Downloaded: 3776 file(s) [attempted 3776/8459 = 44%, 288 KB/s], Decompressed: 3773
Downloaded: 3821 file(s) [attempted 3821/8459 = 45%, 157 KB/s], Decompressed: 3817
Downloaded: 3855 file(s) [attempted 3855/8459 = 45%, 1422 KB/s], Decompressed: 3852
Downloaded: 3900 file(s) [attempted 3900/8459 = 46%, 127 KB/s], Decompressed: 3896
Downloaded: 3937 file(s) [attempted 3937/8459 = 46%, 40 KB/s], Decompressed: 3930
Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 165 KB/s], Decompressed: 3971
Downloaded: 4016 file(s) [attempted 4016/8459 = 47%, 42 KB/s], Decompressed: 4002
Downloaded: 4057 file(s) [attempted 4057/8459 = 47%, 261 KB/s], Decompressed: 4054
Downloaded: 4101 file(s) [attempted 4101/8459 = 48%, 338 KB/s], Decompressed: 4098
Downloaded: 4146 file(s) [attempted 4146/8459 = 49%, 63 KB/s], Decompressed: 4143
Downloaded: 4184 file(s) [attempted 4184/8459 = 49%, 294 KB/s], Decompressed: 4180
Downloaded: 4221 file(s) [attempted 4221/8459 = 49%, 422 KB/s], Decompressed: 4218
Downloaded: 4259 file(s) [attempted 4259/8459 = 50%, 444 KB/s], Decompressed: 4252
Downloaded: 4297 file(s) [attempted 4297/8459 = 50%, 683 KB/s], Decompressed: 4293
Downloaded: 4339 file(s) [attempted 4339/8459 = 51%, 165 KB/s], Decompressed: 4334
Downloaded: 4372 file(s) [attempted 4372/8459 = 51%, 800 KB/s], Decompressed: 4368
Downloaded: 4413 file(s) [attempted 4413/8459 = 52%, 546 KB/s], Decompressed: 4399
Downloaded: 4451 file(s) [attempted 4451/8459 = 52%, 26 KB/s], Decompressed: 4444
Downloaded: 4492 file(s) [attempted 4492/8459 = 53%, 234 KB/s], Decompressed: 4488
Downloaded: 4530 file(s) [attempted 4530/8459 = 53%, 442 KB/s], Decompressed: 4519
Downloaded: 4567 file(s) [attempted 4567/8459 = 53%, 720 KB/s], Decompressed: 4564
Downloaded: 4610 file(s) [attempted 4610/8459 = 54%, 375 KB/s], Decompressed: 4601
Downloaded: 4649 file(s) [attempted 4649/8459 = 54%, 363 KB/s], Decompressed: 4646
Downloaded: 4690 file(s) [attempted 4690/8459 = 55%, 97 KB/s], Decompressed: 4683
Downloaded: 4731 file(s) [attempted 4731/8459 = 55%, 204 KB/s], Decompressed: 4728
Downloaded: 4769 file(s) [attempted 4769/8459 = 56%, 370 KB/s], Decompressed: 4762
Downloaded: 4807 file(s) [attempted 4807/8459 = 56%, 94 KB/s], Decompressed: 4803
Downloaded: 4848 file(s) [attempted 4848/8459 = 57%, 81 KB/s], Decompressed: 4837
Downloaded: 4892 file(s) [attempted 4892/8459 = 57%, 45 KB/s], Decompressed: 4886
Downloaded: 4930 file(s) [attempted 4930/8459 = 58%, 462 KB/s], Decompressed: 4919
Downloaded: 4967 file(s) [attempted 4967/8459 = 58%, 309 KB/s], Decompressed: 4966
Downloaded: 5008 file(s) [attempted 5008/8459 = 59%, 128 KB/s], Decompressed: 5005
Downloaded: 5053 file(s) [attempted 5053/8459 = 59%, 207 KB/s], Decompressed: 5050
Downloaded: 5096 file(s) [attempted 5096/8459 = 60%, 370 KB/s], Decompressed: 5091
Downloaded: 5138 file(s) [attempted 5138/8459 = 60%, 60 KB/s], Decompressed: 5135
Downloaded: 5173 file(s) [attempted 5173/8459 = 61%, 111 KB/s], Decompressed: 5169
Downloaded: 5214 file(s) [attempted 5214/8459 = 61%, 130 KB/s], Decompressed: 5210
Downloaded: 5251 file(s) [attempted 5251/8459 = 62%, 265 KB/s], Decompressed: 5248
Downloaded: 5296 file(s) [attempted 5296/8459 = 62%, 56 KB/s], Decompressed: 5293
Downloaded: 5337 file(s) [attempted 5337/8459 = 63%, 81 KB/s], Decompressed: 5323
Downloaded: 5371 file(s) [attempted 5371/8459 = 63%, 392 KB/s], Decompressed: 5364
Downloaded: 5412 file(s) [attempted 5412/8459 = 63%, 233 KB/s], Decompressed: 5402
Downloaded: 5450 file(s) [attempted 5450/8459 = 64%, 348 KB/s], Decompressed: 5447
Downloaded: 5494 file(s) [attempted 5494/8459 = 64%, 594 KB/s], Decompressed: 5491
Downloaded: 5529 file(s) [attempted 5529/8459 = 65%, 945 KB/s], Decompressed: 5518
Downloaded: 5570 file(s) [attempted 5570/8459 = 65%, 135 KB/s], Decompressed: 5566
Downloaded: 5611 file(s) [attempted 5611/8459 = 66%, 134 KB/s], Decompressed: 5601
Downloaded: 5648 file(s) [attempted 5648/8459 = 66%, 619 KB/s], Decompressed: 5631
Downloaded: 5693 file(s) [attempted 5693/8459 = 67%, 204 KB/s], Decompressed: 5679
Downloaded: 5727 file(s) [attempted 5727/8459 = 67%, 683 KB/s], Decompressed: 5724
Downloaded: 5772 file(s) [attempted 5772/8459 = 68%, 114 KB/s], Decompressed: 5768
Downloaded: 5811 file(s) [attempted 5811/8459 = 68%, 275 KB/s], Decompressed: 5802
Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 639 KB/s], Decompressed: 5840
Downloaded: 5891 file(s) [attempted 5891/8459 = 69%, 297 KB/s], Decompressed: 5888
Downloaded: 5929 file(s) [attempted 5929/8459 = 70%, 1072 KB/s], Decompressed: 5926
Downloaded: 5970 file(s) [attempted 5970/8459 = 70%, 43 KB/s], Decompressed: 5963
Downloaded: 6011 file(s) [attempted 6011/8459 = 71%, 610 KB/s], Decompressed: 6008
Downloaded: 6050 file(s) [attempted 6050/8459 = 71%, 38 KB/s], Decompressed: 6045
Downloaded: 6093 file(s) [attempted 6093/8459 = 72%, 1229 KB/s], Decompressed: 6086
Downloaded: 6138 file(s) [attempted 6138/8459 = 72%, 224 KB/s], Decompressed: 6128
Downloaded: 6175 file(s) [attempted 6175/8459 = 72%, 483 KB/s], Decompressed: 6169
Downloaded: 6213 file(s) [attempted 6213/8459 = 73%, 733 KB/s], Decompressed: 6210
Downloaded: 6251 file(s) [attempted 6251/8459 = 73%, 201 KB/s], Decompressed: 6244
Downloaded: 6296 file(s) [attempted 6296/8459 = 74%, 235 KB/s], Decompressed: 6292
Downloaded: 6340 file(s) [attempted 6340/8459 = 74%, 2962 KB/s], Decompressed: 6336
Downloaded: 6381 file(s) [attempted 6381/8459 = 75%, 283 KB/s], Decompressed: 6377
Downloaded: 6421 file(s) [attempted 6421/8459 = 75%, 147 KB/s], Decompressed: 6405
Downloaded: 6449 file(s) [attempted 6449/8459 = 76%, 242 KB/s], Decompressed: 6446
Downloaded: 6497 file(s) [attempted 6497/8459 = 76%, 73 KB/s], Decompressed: 6494
Downloaded: 6545 file(s) [attempted 6545/8459 = 77%, 326 KB/s], Decompressed: 6542
Downloaded: 6593 file(s) [attempted 6593/8459 = 77%, 457 KB/s], Decompressed: 6586
Downloaded: 6641 file(s) [attempted 6641/8459 = 78%, 223 KB/s], Decompressed: 6634
Downloaded: 6684 file(s) [attempted 6684/8459 = 79%, 242 KB/s], Decompressed: 6675
Downloaded: 6716 file(s) [attempted 6716/8459 = 79%, 235 KB/s], Decompressed: 6706
Downloaded: 6751 file(s) [attempted 6751/8459 = 79%, 505 KB/s], Decompressed: 6747
Downloaded: 6795 file(s) [attempted 6795/8459 = 80%, 279 KB/s], Decompressed: 6792
Downloaded: 6838 file(s) [attempted 6838/8459 = 80%, 269 KB/s], Decompressed: 6829
Downloaded: 6877 file(s) [attempted 6877/8459 = 81%, 597 KB/s], Decompressed: 6867
Downloaded: 6906 file(s) [attempted 6906/8459 = 81%, 315 KB/s], Decompressed: 6901
Downloaded: 6949 file(s) [attempted 6949/8459 = 82%, 206 KB/s], Decompressed: 6946
Downloaded: 6994 file(s) [attempted 6994/8459 = 82%, 2105 KB/s], Decompressed: 6990
Downloaded: 7033 file(s) [attempted 7033/8459 = 83%, 976 KB/s], Decompressed: 7024
Downloaded: 7065 file(s) [attempted 7065/8459 = 83%, 1152 KB/s], Decompressed: 7062
Downloaded: 7103 file(s) [attempted 7103/8459 = 83%, 361 KB/s], Decompressed: 7100
Downloaded: 7144 file(s) [attempted 7144/8459 = 84%, 428 KB/s], Decompressed: 7137
Downloaded: 7189 file(s) [attempted 7189/8459 = 84%, 673 KB/s], Decompressed: 7178
Downloaded: 7226 file(s) [attempted 7226/8459 = 85%, 125 KB/s], Decompressed: 7223
Downloaded: 7267 file(s) [attempted 7267/8459 = 85%, 815 KB/s], Decompressed: 7257
Downloaded: 7300 file(s) [attempted 7300/8459 = 86%, 167 KB/s], Decompressed: 7295
Downloaded: 7343 file(s) [attempted 7343/8459 = 86%, 104 KB/s], Decompressed: 7339
Downloaded: 7380 file(s) [attempted 7380/8459 = 87%, 601 KB/s], Decompressed: 7374
Downloaded: 7425 file(s) [attempted 7425/8459 = 87%, 502 KB/s], Decompressed: 7421
Downloaded: 7473 file(s) [attempted 7473/8459 = 88%, 96 KB/s], Decompressed: 7469
Downloaded: 7511 file(s) [attempted 7511/8459 = 88%, 201 KB/s], Decompressed: 7500
Downloaded: 7545 file(s) [attempted 7545/8459 = 89%, 113 KB/s], Decompressed: 7538
Downloaded: 7586 file(s) [attempted 7586/8459 = 89%, 116 KB/s], Decompressed: 7582
Downloaded: 7630 file(s) [attempted 7630/8459 = 90%, 210 KB/s], Decompressed: 7627
Downloaded: 7671 file(s) [attempted 7671/8459 = 90%, 37 KB/s], Decompressed: 7668
Downloaded: 7712 file(s) [attempted 7712/8459 = 91%, 75 KB/s], Decompressed: 7709
Downloaded: 7743 file(s) [attempted 7743/8459 = 91%, 153 KB/s], Decompressed: 7736
Downloaded: 7784 file(s) [attempted 7784/8459 = 92%, 30 KB/s], Decompressed: 7777
Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 156 KB/s], Decompressed: 7815
Downloaded: 7863 file(s) [attempted 7863/8459 = 92%, 667 KB/s], Decompressed: 7859
Downloaded: 7904 file(s) [attempted 7904/8459 = 93%, 776 KB/s], Decompressed: 7897
Downloaded: 7948 file(s) [attempted 7948/8459 = 93%, 514 KB/s], Decompressed: 7945
Downloaded: 7989 file(s) [attempted 7989/8459 = 94%, 1471 KB/s], Decompressed: 7986
Downloaded: 8027 file(s) [attempted 8027/8459 = 94%, 1885 KB/s], Decompressed: 8024
Downloaded: 8068 file(s) [attempted 8068/8459 = 95%, 34 KB/s], Decompressed: 8061
Downloaded: 8106 file(s) [attempted 8106/8459 = 95%, 245 KB/s], Decompressed: 8099
Downloaded: 8147 file(s) [attempted 8147/8459 = 96%, 173 KB/s], Decompressed: 8143
Downloaded: 8188 file(s) [attempted 8188/8459 = 96%, 264 KB/s], Decompressed: 8185
Downloaded: 8226 file(s) [attempted 8226/8459 = 97%, 291 KB/s], Decompressed: 8222
Downloaded: 8263 file(s) [attempted 8263/8459 = 97%, 893 KB/s], Decompressed: 8256
Downloaded: 8301 file(s) [attempted 8301/8459 = 98%, 2769 KB/s], Decompressed: 8297
Downloaded: 8345 file(s) [attempted 8345/8459 = 98%, 982 KB/s], Decompressed: 8342
Downloaded: 8386 file(s) [attempted 8386/8459 = 99%, 86 KB/s], Decompressed: 8376
Downloaded: 8424 file(s) [attempted 8424/8459 = 99%, 261 KB/s], Decompressed: 8421
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 510 KB/s], Decompressed: 8452
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 510 KB/s], Decompressed: 8452

lake build

✔ [3471/3476] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (19s)
✔ [3473/3476] Built PrimeNumberTheoremAnd.ZetaBounds (64s)
✔ [3486/3499] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit (3.7s)
✔ [3533/3544] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth (2.5s)
ℹ [3535/3547] Built PrimeNumberTheoremAnd.MediumPNT (35s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3563/3571] Built PrimeNumberTheoremAnd.StrongPNT (16s)
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`
✔ [3567/3573] Built PrimeNumberTheoremAnd.BorelCaratheodory (4.8s)
⚠ [3698/3711] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3805/3818] Built PrimeNumberTheoremAnd.IEANTN.LogTables (27s)
⚠ [3811/3818] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3814/3819] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv (2.2s)
⚠ [3816/3819] Built PrimeNumberTheoremAnd.IEANTN.Mertens (15s)
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:925:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:929:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:939:8: declaration uses `sorry`
✔ [3817/3820] Built PrimeNumberTheoremAnd.EulerMascheroniBounds (10s)
✔ [3875/3890] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables (2.7s)
⚠ [3880/3892] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (61s)
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.3s)
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`
✔ [3886/3894] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (4.4s)
✔ [3887/3895] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (3.2s)
✔ [3891/3895] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (6.7s)
⚠ [3892/3895] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (6.2s)
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/3899] Built PrimeNumberTheoremAnd.IEANTN.CostaPereira (9.5s)
⚠ [4014/4022] Built PrimeNumberTheoremAnd.IEANTN.Buthe (12s)
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`
✔ [4017/4025] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables (55s)
⚠ [4018/4025] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (17s)
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`
✔ [4019/4025] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (92s)
⚠ [4020/4026] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (16s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4022/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (31s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
✔ [4033/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (5.7s)
ℹ [4055/4068] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (58s)
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/4068] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (4.3s)
✔ [4059/4072] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (2.7s)
⚠ [4060/4072] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (15s)
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`
⚠ [4063/4074] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP (22s)
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`
✔ [4066/4074] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (17s)
⚠ [4068/4074] Built PrimeNumberTheoremAnd.IEANTN.Dusart (18s)
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`
✔ [4071/4074] Built PrimeNumberTheoremAnd.IEANTN.Erdos392 (53s)
⚠ [4073/4101] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (70s)
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`
⚠ [4105/4118] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4107/4118] 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`
⚠ [4121/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/4161] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (10s)
⚠ [4127/4166] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (15s)
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`
✔ [4131/4166] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial (2.2s)
✔ [4138/4166] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Real (2.2s)
✔ [4144/4180] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation (2.3s)
⚠ [4147/4186] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (9.9s)
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`
ℹ [4155/4186] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations (20s)
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.
⚠ [4156/4186] 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`
✔ [4159/4186] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (13s)
⚠ [4160/4186] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (6.6s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4167/4186] Built PrimeNumberTheoremAnd.IEANTN.Lcm (29s)
✔ [4168/4186] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (57s)
✔ [4169/4186] Built PrimeNumberTheoremAnd.LaplaceInversion (4.6s)
✔ [4171/4186] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (2.9s)
⚠ [4184/4186] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (14s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:167:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:275:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:355:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:714:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:792:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:879:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:962:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2192:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2824:8: declaration uses `sorry`
✔ [4185/4186] Built PrimeNumberTheoremAnd (6.2s)
Build completed successfully (4186 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 (765ms)
✔ [26/35] Built Cli.Basic:c.o (3.1s)
✔ [30/35] Built Cli.Extensions:c.o (503ms)
✔ [33/39] Built Cli:c.o (65ms)
✔ [3506/3518] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds:blueprint (3.9s)
✔ [3509/3549] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (65s)
✔ [3526/3549] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit:blueprint (2.6s)
✔ [3591/3610] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth:blueprint (2.2s)
ℹ [3593/3610] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3595/3611] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (57s)
⚠ [3626/3642] 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`
✔ [3631/3643] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (48s)
✔ [3637/3650] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (6.7s)
⚠ [3766/3784] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3879/3900] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (2.7s)
⚠ [3885/3900] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3895/3901] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:925:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:929:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:939:8: declaration uses `sorry`
✔ [3896/3901] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv:blueprint (2.3s)
✔ [3899/3906] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMascheroniBounds:blueprint (2.6s)
✔ [3900/3906] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (34s)
✔ [3956/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (2.6s)
⚠ [3960/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 `⊢`!
⚠ [3962/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/3987] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (26s)
⚠ [3968/3987] 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.5s)
✔ [3976/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Li2Bounds:blueprint (5.0s)
✔ [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.7s)
⚠ [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/4125] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (6.3s)
⚠ [4113/4126] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
✔ [4114/4126] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables:blueprint (2.0s)
⚠ [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/4177] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (20s)
✔ [4120/4177] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (17s)
✔ [4121/4177] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (4.8s)
⚠ [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 (5.0s)
ℹ [4143/4198] 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.
✔ [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.6s)
✔ [4183/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables:blueprint (2.7s)
⚠ [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`
✔ [4188/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (19s)
✔ [4190/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP:blueprint (3.4s)
⚠ [4191/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`
✔ [4197/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (18s)
✔ [4198/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (19s)
⚠ [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`
✔ [4204/4251] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (16s)
✔ [4205/4251] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (32s)
⚠ [4247/4267] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4253/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`
⚠ [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/4383] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (3.2s)
⚠ [4280/4383] 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/4393] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (44s)
⚠ [4300/4393] 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`
✔ [4306/4393] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial:blueprint (2.3s)
✔ [4315/4393] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Real:blueprint (2.3s)
✔ [4322/4393] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation:blueprint (2.7s)
ℹ [4326/4393] 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.
⚠ [4327/4393] 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`
✔ [4331/4393] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (6.9s)
⚠ [4332/4393] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4345/4393] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations:blueprint (7.8s)
✔ [4352/4393] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (10s)
✔ [4354/4393] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (6.2s)
✔ [4379/4393] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (11s)
✔ [4380/4393] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (3.2s)
✔ [4381/4393] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (15s)
✔ [4382/4393] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.LaplaceInversion:blueprint (2.7s)
⚠ [4388/4393] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:167:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:275:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:355:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:714:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:792:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:879:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:962:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2192:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2824:8: declaration uses `sorry`
✔ [4389/4393] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (44s)
✔ [4391/4394] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (6.2s)
ℹ [4392/4394] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (83ms)
info: Blueprint indexing
Build completed successfully (4394 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)

apx-semantic-phase	{"duration_ms":2,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":87,"diagnostic_count":57,"duration_ms":6230,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase	{"declaration_count":87,"dependency_count":33,"diagnostic_count":57,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":819059,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase	{"declaration_count":87,"dependency_count":33,"diagnostic_count":57,"duration_ms":77,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":0,"ok":true,"payload_bytes":629510,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":5,"ok":true,"payload_bytes":629510,"phase":"lean_json_write"}

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":"core_compile","duration_ms":6617}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":276,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
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":"runner_compile","duration_ms":33311,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 6428055e38a3e996ca2e96ecc9af612d49a13b50ce301d1c4d8b6430d2321147
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":839401,"ok":true}