Run 163

git fetch --depth 1 origin d30f67d5929e9755bff3447bfdd853030ece56a9

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

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

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

git checkout d30f67d5929e9755bff3447bfdd853030ece56a9

fatal: reference is not a tree: d30f67d5929e9755bff3447bfdd853030ece56a9

git checkout d30f67d5929e9755bff3447bfdd853030ece56a9 (after fetch)

Note: switching to 'd30f67d5929e9755bff3447bfdd853030ece56a9'.

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 d30f67d fix build errprs in Mertens (#1613)

lake exe cache get

Current branch: HEAD
Using cache from origin: (some leanprover-community/mathlib4)
Attempting to download 8546 file(s) from leanprover-community/mathlib4 cache at https://lakecache.blob.core.windows.net/mathlib4-master
Decompressed 8546 file(s)
Already decompressed 8546 file(s)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
info: leancert: cloning https://github.com/kim-em/leancert.git
info: leancert: checking out revision '41cb6b59a7c06622b327cf23eaf5f4331a655fd9'
info: LeanArchitect: cloning https://github.com/hanwenzhu/LeanArchitect.git
info: LeanArchitect: checking out revision '8f56f86dcec03fa46cd21b0f7bee4d724f68dcc4'
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

Downloaded: 1 file(s) [attempted 1/8546 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 16 file(s) [attempted 16/8546 = 0%, 1 KB/s], Decompressed: 15
Downloaded: 39 file(s) [attempted 39/8546 = 0%, 29 KB/s], Decompressed: 38
Downloaded: 67 file(s) [attempted 67/8546 = 0%, 47 KB/s], Decompressed: 60
Downloaded: 88 file(s) [attempted 88/8546 = 1%, 188 KB/s], Decompressed: 81
Downloaded: 116 file(s) [attempted 116/8546 = 1%, 77 KB/s], Decompressed: 112
Downloaded: 143 file(s) [attempted 143/8546 = 1%, 382 KB/s], Decompressed: 139
Downloaded: 183 file(s) [attempted 183/8546 = 2%, 150 KB/s], Decompressed: 180
Downloaded: 217 file(s) [attempted 217/8546 = 2%, 493 KB/s], Decompressed: 214
Downloaded: 253 file(s) [attempted 253/8546 = 2%, 119 KB/s], Decompressed: 248
Downloaded: 290 file(s) [attempted 290/8546 = 3%, 81 KB/s], Decompressed: 282
Downloaded: 326 file(s) [attempted 326/8546 = 3%, 147 KB/s], Decompressed: 319
Downloaded: 366 file(s) [attempted 366/8546 = 4%, 426 KB/s], Decompressed: 360
Downloaded: 407 file(s) [attempted 407/8546 = 4%, 181 KB/s], Decompressed: 400
Downloaded: 442 file(s) [attempted 442/8546 = 5%, 733 KB/s], Decompressed: 434
Downloaded: 480 file(s) [attempted 480/8546 = 5%, 1262 KB/s], Decompressed: 475
Downloaded: 522 file(s) [attempted 522/8546 = 6%, 1098 KB/s], Decompressed: 519
Downloaded: 566 file(s) [attempted 566/8546 = 6%, 255 KB/s], Decompressed: 559
Downloaded: 603 file(s) [attempted 603/8546 = 7%, 261 KB/s], Decompressed: 600
Downloaded: 642 file(s) [attempted 642/8546 = 7%, 215 KB/s], Decompressed: 637
Downloaded: 681 file(s) [attempted 681/8546 = 7%, 64 KB/s], Decompressed: 678
Downloaded: 725 file(s) [attempted 725/8546 = 8%, 247 KB/s], Decompressed: 718
Downloaded: 766 file(s) [attempted 766/8546 = 8%, 602 KB/s], Decompressed: 762
Downloaded: 807 file(s) [attempted 807/8546 = 9%, 24 KB/s], Decompressed: 800
Downloaded: 840 file(s) [attempted 840/8546 = 9%, 418 KB/s], Decompressed: 834
Downloaded: 881 file(s) [attempted 881/8546 = 10%, 42 KB/s], Decompressed: 874
Downloaded: 925 file(s) [attempted 925/8546 = 10%, 51 KB/s], Decompressed: 918
Downloaded: 968 file(s) [attempted 968/8546 = 11%, 402 KB/s], Decompressed: 959
Downloaded: 1003 file(s) [attempted 1003/8546 = 11%, 137 KB/s], Decompressed: 999
Downloaded: 1043 file(s) [attempted 1043/8546 = 12%, 642 KB/s], Decompressed: 1033
Downloaded: 1084 file(s) [attempted 1084/8546 = 12%, 212 KB/s], Decompressed: 1081
Downloaded: 1128 file(s) [attempted 1128/8546 = 13%, 438 KB/s], Decompressed: 1125
Downloaded: 1167 file(s) [attempted 1167/8546 = 13%, 457 KB/s], Decompressed: 1158
Downloaded: 1206 file(s) [attempted 1206/8546 = 14%, 925 KB/s], Decompressed: 1202
Downloaded: 1246 file(s) [attempted 1246/8546 = 14%, 1260 KB/s], Decompressed: 1240
Downloaded: 1287 file(s) [attempted 1287/8546 = 15%, 269 KB/s], Decompressed: 1273
Downloaded: 1325 file(s) [attempted 1325/8546 = 15%, 505 KB/s], Decompressed: 1321
Downloaded: 1365 file(s) [attempted 1365/8546 = 15%, 634 KB/s], Decompressed: 1361
Downloaded: 1409 file(s) [attempted 1409/8546 = 16%, 118 KB/s], Decompressed: 1399
Downloaded: 1449 file(s) [attempted 1449/8546 = 16%, 519 KB/s], Decompressed: 1443
Downloaded: 1487 file(s) [attempted 1487/8546 = 17%, 25 KB/s], Decompressed: 1483
Downloaded: 1527 file(s) [attempted 1527/8546 = 17%, 372 KB/s], Decompressed: 1517
Downloaded: 1571 file(s) [attempted 1571/8546 = 18%, 247 KB/s], Decompressed: 1564
Downloaded: 1608 file(s) [attempted 1608/8546 = 18%, 22 KB/s], Decompressed: 1605
Downloaded: 1652 file(s) [attempted 1652/8546 = 19%, 438 KB/s], Decompressed: 1649
Downloaded: 1696 file(s) [attempted 1696/8546 = 19%, 346 KB/s], Decompressed: 1689
Downloaded: 1740 file(s) [attempted 1740/8546 = 20%, 116 KB/s], Decompressed: 1733
Downloaded: 1784 file(s) [attempted 1784/8546 = 20%, 93 KB/s], Decompressed: 1777
Downloaded: 1826 file(s) [attempted 1826/8546 = 21%, 322 KB/s], Decompressed: 1821
Downloaded: 1865 file(s) [attempted 1865/8546 = 21%, 86 KB/s], Decompressed: 1859
Downloaded: 1903 file(s) [attempted 1903/8546 = 22%, 1419 KB/s], Decompressed: 1899
Downloaded: 1937 file(s) [attempted 1937/8546 = 22%, 807 KB/s], Decompressed: 1933
Downloaded: 1980 file(s) [attempted 1980/8546 = 23%, 127 KB/s], Decompressed: 1977
Downloaded: 2024 file(s) [attempted 2024/8546 = 23%, 2778 KB/s], Decompressed: 2021
Downloaded: 2065 file(s) [attempted 2065/8546 = 24%, 909 KB/s], Decompressed: 2058
Downloaded: 2102 file(s) [attempted 2102/8546 = 24%, 234 KB/s], Decompressed: 2099
Downloaded: 2143 file(s) [attempted 2143/8546 = 25%, 1481 KB/s], Decompressed: 2136
Downloaded: 2183 file(s) [attempted 2183/8546 = 25%, 328 KB/s], Decompressed: 2180
Downloaded: 2224 file(s) [attempted 2224/8546 = 26%, 523 KB/s], Decompressed: 2221
Downloaded: 2265 file(s) [attempted 2265/8546 = 26%, 312 KB/s], Decompressed: 2258
Downloaded: 2302 file(s) [attempted 2302/8546 = 26%, 345 KB/s], Decompressed: 2295
Downloaded: 2342 file(s) [attempted 2342/8546 = 27%, 326 KB/s], Decompressed: 2339
Downloaded: 2383 file(s) [attempted 2383/8546 = 27%, 359 KB/s], Decompressed: 2380
Downloaded: 2426 file(s) [attempted 2426/8546 = 28%, 49 KB/s], Decompressed: 2418
Downloaded: 2460 file(s) [attempted 2460/8546 = 28%, 183 KB/s], Decompressed: 2454
Downloaded: 2501 file(s) [attempted 2501/8546 = 29%, 465 KB/s], Decompressed: 2491
Downloaded: 2536 file(s) [attempted 2536/8546 = 29%, 248 KB/s], Decompressed: 2532
Downloaded: 2579 file(s) [attempted 2579/8546 = 30%, 127 KB/s], Decompressed: 2576
Downloaded: 2623 file(s) [attempted 2623/8546 = 30%, 22 KB/s], Decompressed: 2620
Downloaded: 2667 file(s) [attempted 2667/8546 = 31%, 24 KB/s], Decompressed: 2664
Downloaded: 2711 file(s) [attempted 2711/8546 = 31%, 417 KB/s], Decompressed: 2708
Downloaded: 2755 file(s) [attempted 2755/8546 = 32%, 382 KB/s], Decompressed: 2745
Downloaded: 2782 file(s) [attempted 2782/8546 = 32%, 387 KB/s], Decompressed: 2779
Downloaded: 2826 file(s) [attempted 2826/8546 = 33%, 276 KB/s], Decompressed: 2823
Downloaded: 2868 file(s) [attempted 2868/8546 = 33%, 333 KB/s], Decompressed: 2863
Downloaded: 2911 file(s) [attempted 2911/8546 = 34%, 573 KB/s], Decompressed: 2904
Downloaded: 2955 file(s) [attempted 2955/8546 = 34%, 81 KB/s], Decompressed: 2951
Downloaded: 2994 file(s) [attempted 2994/8546 = 35%, 1203 KB/s], Decompressed: 2985
Downloaded: 3032 file(s) [attempted 3032/8546 = 35%, 715 KB/s], Decompressed: 3029
Downloaded: 3073 file(s) [attempted 3073/8546 = 35%, 159 KB/s], Decompressed: 3070
Downloaded: 3114 file(s) [attempted 3114/8546 = 36%, 293 KB/s], Decompressed: 3110
Downloaded: 3158 file(s) [attempted 3158/8546 = 36%, 152 KB/s], Decompressed: 3151
Downloaded: 3200 file(s) [attempted 3200/8546 = 37%, 86 KB/s], Decompressed: 3191
Downloaded: 3236 file(s) [attempted 3236/8546 = 37%, 619 KB/s], Decompressed: 3229
Downloaded: 3279 file(s) [attempted 3279/8546 = 38%, 569 KB/s], Decompressed: 3276
Downloaded: 3327 file(s) [attempted 3327/8546 = 38%, 626 KB/s], Decompressed: 3320
Downloaded: 3368 file(s) [attempted 3368/8546 = 39%, 60 KB/s], Decompressed: 3361
Downloaded: 3408 file(s) [attempted 3408/8546 = 39%, 49 KB/s], Decompressed: 3405
Downloaded: 3448 file(s) [attempted 3448/8546 = 40%, 312 KB/s], Decompressed: 3445
Downloaded: 3486 file(s) [attempted 3486/8546 = 40%, 634 KB/s], Decompressed: 3482
Downloaded: 3530 file(s) [attempted 3530/8546 = 41%, 105 KB/s], Decompressed: 3520
Downloaded: 3570 file(s) [attempted 3570/8546 = 41%, 827 KB/s], Decompressed: 3560
Downloaded: 3611 file(s) [attempted 3611/8546 = 42%, 691 KB/s], Decompressed: 3597
Downloaded: 3655 file(s) [attempted 3655/8546 = 42%, 1234 KB/s], Decompressed: 3648
Downloaded: 3697 file(s) [attempted 3697/8546 = 43%, 104 KB/s], Decompressed: 3685
Downloaded: 3736 file(s) [attempted 3736/8546 = 43%, 299 KB/s], Decompressed: 3729
Downloaded: 3777 file(s) [attempted 3777/8546 = 44%, 745 KB/s], Decompressed: 3773
Downloaded: 3817 file(s) [attempted 3817/8546 = 44%, 476 KB/s], Decompressed: 3814
Downloaded: 3860 file(s) [attempted 3860/8546 = 45%, 343 KB/s], Decompressed: 3854
Downloaded: 3902 file(s) [attempted 3902/8546 = 45%, 275 KB/s], Decompressed: 3888
Downloaded: 3936 file(s) [attempted 3936/8546 = 46%, 361 KB/s], Decompressed: 3932
Downloaded: 3981 file(s) [attempted 3981/8546 = 46%, 232 KB/s], Decompressed: 3973
Downloaded: 4020 file(s) [attempted 4020/8546 = 47%, 699 KB/s], Decompressed: 4013
Downloaded: 4064 file(s) [attempted 4064/8546 = 47%, 770 KB/s], Decompressed: 4057
Downloaded: 4105 file(s) [attempted 4105/8546 = 48%, 1208 KB/s], Decompressed: 4101
Downloaded: 4145 file(s) [attempted 4145/8546 = 48%, 216 KB/s], Decompressed: 4139
Downloaded: 4186 file(s) [attempted 4186/8546 = 48%, 50 KB/s], Decompressed: 4176
Downloaded: 4223 file(s) [attempted 4223/8546 = 49%, 1335 KB/s], Decompressed: 4220
Downloaded: 4267 file(s) [attempted 4267/8546 = 49%, 369 KB/s], Decompressed: 4257
Downloaded: 4304 file(s) [attempted 4304/8546 = 50%, 253 KB/s], Decompressed: 4301
Downloaded: 4348 file(s) [attempted 4348/8546 = 50%, 957 KB/s], Decompressed: 4345
Downloaded: 4389 file(s) [attempted 4389/8546 = 51%, 249 KB/s], Decompressed: 4382
Downloaded: 4430 file(s) [attempted 4430/8546 = 51%, 100 KB/s], Decompressed: 4426
Downloaded: 4470 file(s) [attempted 4470/8546 = 52%, 313 KB/s], Decompressed: 4463
Downloaded: 4507 file(s) [attempted 4507/8546 = 52%, 572 KB/s], Decompressed: 4504
Downloaded: 4553 file(s) [attempted 4553/8546 = 53%, 75 KB/s], Decompressed: 4545
Downloaded: 4595 file(s) [attempted 4595/8546 = 53%, 48 KB/s], Decompressed: 4582
Downloaded: 4634 file(s) [attempted 4634/8546 = 54%, 362 KB/s], Decompressed: 4626
Downloaded: 4673 file(s) [attempted 4673/8546 = 54%, 1052 KB/s], Decompressed: 4666
Downloaded: 4714 file(s) [attempted 4714/8546 = 55%, 71 KB/s], Decompressed: 4710
Downloaded: 4758 file(s) [attempted 4758/8546 = 55%, 345 KB/s], Decompressed: 4754
Downloaded: 4798 file(s) [attempted 4798/8546 = 56%, 23 KB/s], Decompressed: 4791
Downloaded: 4839 file(s) [attempted 4839/8546 = 56%, 496 KB/s], Decompressed: 4829
Downloaded: 4876 file(s) [attempted 4876/8546 = 57%, 124 KB/s], Decompressed: 4869
Downloaded: 4917 file(s) [attempted 4917/8546 = 57%, 185 KB/s], Decompressed: 4913
Downloaded: 4961 file(s) [attempted 4961/8546 = 58%, 217 KB/s], Decompressed: 4954
Downloaded: 5005 file(s) [attempted 5005/8546 = 58%, 192 KB/s], Decompressed: 5003
Downloaded: 5045 file(s) [attempted 5045/8546 = 59%, 91 KB/s], Decompressed: 5042
Downloaded: 5089 file(s) [attempted 5089/8546 = 59%, 545 KB/s], Decompressed: 5086
Downloaded: 5131 file(s) [attempted 5131/8546 = 60%, 160 KB/s], Decompressed: 5120
Downloaded: 5162 file(s) [attempted 5162/8546 = 60%, 128 KB/s], Decompressed: 5157
Downloaded: 5204 file(s) [attempted 5204/8546 = 60%, 234 KB/s], Decompressed: 5197
Downloaded: 5245 file(s) [attempted 5245/8546 = 61%, 162 KB/s], Decompressed: 5238
Downloaded: 5285 file(s) [attempted 5285/8546 = 61%, 203 KB/s], Decompressed: 5282
Downloaded: 5329 file(s) [attempted 5329/8546 = 62%, 116 KB/s], Decompressed: 5326
Downloaded: 5370 file(s) [attempted 5370/8546 = 62%, 312 KB/s], Decompressed: 5367
Downloaded: 5408 file(s) [attempted 5408/8546 = 63%, 105 KB/s], Decompressed: 5404
Downloaded: 5448 file(s) [attempted 5448/8546 = 63%, 24 KB/s], Decompressed: 5444
Downloaded: 5488 file(s) [attempted 5488/8546 = 64%, 196 KB/s], Decompressed: 5485
Downloaded: 5532 file(s) [attempted 5532/8546 = 64%, 23 KB/s], Decompressed: 5529
Downloaded: 5573 file(s) [attempted 5573/8546 = 65%, 98 KB/s], Decompressed: 5556
Downloaded: 5612 file(s) [attempted 5612/8546 = 65%, 387 KB/s], Decompressed: 5603
Downloaded: 5647 file(s) [attempted 5647/8546 = 66%, 1037 KB/s], Decompressed: 5641
Downloaded: 5688 file(s) [attempted 5688/8546 = 66%, 45 KB/s], Decompressed: 5685
Downloaded: 5735 file(s) [attempted 5735/8546 = 67%, 49 KB/s], Decompressed: 5732
Downloaded: 5781 file(s) [attempted 5781/8546 = 67%, 175 KB/s], Decompressed: 5769
Downloaded: 5820 file(s) [attempted 5820/8546 = 68%, 205 KB/s], Decompressed: 5816
Downloaded: 5860 file(s) [attempted 5860/8546 = 68%, 362 KB/s], Decompressed: 5857
Downloaded: 5904 file(s) [attempted 5904/8546 = 69%, 123 KB/s], Decompressed: 5898
Downloaded: 5945 file(s) [attempted 5945/8546 = 69%, 761 KB/s], Decompressed: 5942
Downloaded: 5982 file(s) [attempted 5982/8546 = 69%, 116 KB/s], Decompressed: 5962
Downloaded: 6021 file(s) [attempted 6021/8546 = 70%, 262 KB/s], Decompressed: 6009
Downloaded: 6060 file(s) [attempted 6060/8546 = 70%, 238 KB/s], Decompressed: 6053
Downloaded: 6104 file(s) [attempted 6104/8546 = 71%, 59 KB/s], Decompressed: 6101
Downloaded: 6148 file(s) [attempted 6148/8546 = 71%, 341 KB/s], Decompressed: 6145
Downloaded: 6189 file(s) [attempted 6189/8546 = 72%, 884 KB/s], Decompressed: 6185
Downloaded: 6220 file(s) [attempted 6220/8546 = 72%, 993 KB/s], Decompressed: 6216
Downloaded: 6263 file(s) [attempted 6263/8546 = 73%, 425 KB/s], Decompressed: 6256
Downloaded: 6304 file(s) [attempted 6304/8546 = 73%, 636 KB/s], Decompressed: 6297
Downloaded: 6341 file(s) [attempted 6341/8546 = 74%, 183 KB/s], Decompressed: 6337
Downloaded: 6381 file(s) [attempted 6381/8546 = 74%, 200 KB/s], Decompressed: 6378
Downloaded: 6422 file(s) [attempted 6422/8546 = 75%, 302 KB/s], Decompressed: 6415
Downloaded: 6460 file(s) [attempted 6460/8546 = 75%, 463 KB/s], Decompressed: 6452
Downloaded: 6500 file(s) [attempted 6500/8546 = 76%, 88 KB/s], Decompressed: 6493
Downloaded: 6540 file(s) [attempted 6540/8546 = 76%, 278 KB/s], Decompressed: 6537
Downloaded: 6579 file(s) [attempted 6579/8546 = 76%, 160 KB/s], Decompressed: 6574
Downloaded: 6622 file(s) [attempted 6622/8546 = 77%, 52 KB/s], Decompressed: 6615
Downloaded: 6662 file(s) [attempted 6662/8546 = 77%, 436 KB/s], Decompressed: 6655
Downloaded: 6701 file(s) [attempted 6701/8546 = 78%, 64 KB/s], Decompressed: 6693
Downloaded: 6738 file(s) [attempted 6738/8546 = 78%, 209 KB/s], Decompressed: 6733
Downloaded: 6779 file(s) [attempted 6779/8546 = 79%, 174 KB/s], Decompressed: 6774
Downloaded: 6818 file(s) [attempted 6818/8546 = 79%, 90 KB/s], Decompressed: 6811
Downloaded: 6858 file(s) [attempted 6858/8546 = 80%, 509 KB/s], Decompressed: 6855
Downloaded: 6906 file(s) [attempted 6906/8546 = 80%, 92 KB/s], Decompressed: 6902
Downloaded: 6937 file(s) [attempted 6937/8546 = 81%, 1048 KB/s], Decompressed: 6933
Downloaded: 6980 file(s) [attempted 6980/8546 = 81%, 449 KB/s], Decompressed: 6970
Downloaded: 7018 file(s) [attempted 7018/8546 = 82%, 435 KB/s], Decompressed: 7014
Downloaded: 7061 file(s) [attempted 7061/8546 = 82%, 841 KB/s], Decompressed: 7058
Downloaded: 7109 file(s) [attempted 7109/8546 = 83%, 977 KB/s], Decompressed: 7105
Downloaded: 7153 file(s) [attempted 7153/8546 = 83%, 194 KB/s], Decompressed: 7142
Downloaded: 7188 file(s) [attempted 7188/8546 = 84%, 327 KB/s], Decompressed: 7183
Downloaded: 7230 file(s) [attempted 7230/8546 = 84%, 259 KB/s], Decompressed: 7224
Downloaded: 7273 file(s) [attempted 7273/8546 = 85%, 58 KB/s], Decompressed: 7264
Downloaded: 7312 file(s) [attempted 7312/8546 = 85%, 1872 KB/s], Decompressed: 7308
Downloaded: 7356 file(s) [attempted 7356/8546 = 86%, 805 KB/s], Decompressed: 7352
Downloaded: 7393 file(s) [attempted 7393/8546 = 86%, 1143 KB/s], Decompressed: 7383
Downloaded: 7430 file(s) [attempted 7430/8546 = 86%, 114 KB/s], Decompressed: 7427
Downloaded: 7477 file(s) [attempted 7477/8546 = 87%, 240 KB/s], Decompressed: 7467
Downloaded: 7525 file(s) [attempted 7525/8546 = 88%, 605 KB/s], Decompressed: 7518
Downloaded: 7566 file(s) [attempted 7566/8546 = 88%, 136 KB/s], Decompressed: 7548
Downloaded: 7606 file(s) [attempted 7606/8546 = 89%, 129 KB/s], Decompressed: 7599
Downloaded: 7640 file(s) [attempted 7640/8546 = 89%, 589 KB/s], Decompressed: 7633
Downloaded: 7676 file(s) [attempted 7676/8546 = 89%, 161 KB/s], Decompressed: 7670
Downloaded: 7719 file(s) [attempted 7719/8546 = 90%, 1155 KB/s], Decompressed: 7714
Downloaded: 7765 file(s) [attempted 7765/8546 = 90%, 146 KB/s], Decompressed: 7758
Downloaded: 7809 file(s) [attempted 7809/8546 = 91%, 194 KB/s], Decompressed: 7799
Downloaded: 7846 file(s) [attempted 7846/8546 = 91%, 561 KB/s], Decompressed: 7839
Downloaded: 7884 file(s) [attempted 7884/8546 = 92%, 160 KB/s], Decompressed: 7880
Downloaded: 7924 file(s) [attempted 7924/8546 = 92%, 295 KB/s], Decompressed: 7917
Downloaded: 7964 file(s) [attempted 7964/8546 = 93%, 520 KB/s], Decompressed: 7961
Downloaded: 8008 file(s) [attempted 8008/8546 = 93%, 169 KB/s], Decompressed: 8002
Downloaded: 8052 file(s) [attempted 8052/8546 = 94%, 1203 KB/s], Decompressed: 8049
Downloaded: 8088 file(s) [attempted 8088/8546 = 94%, 209 KB/s], Decompressed: 8083
Downloaded: 8130 file(s) [attempted 8130/8546 = 95%, 359 KB/s], Decompressed: 8123
Downloaded: 8167 file(s) [attempted 8167/8546 = 95%, 822 KB/s], Decompressed: 8164
Downloaded: 8215 file(s) [attempted 8215/8546 = 96%, 116 KB/s], Decompressed: 8211
Downloaded: 8262 file(s) [attempted 8262/8546 = 96%, 55 KB/s], Decompressed: 8255
Downloaded: 8299 file(s) [attempted 8299/8546 = 97%, 134 KB/s], Decompressed: 8293
Downloaded: 8340 file(s) [attempted 8340/8546 = 97%, 51 KB/s], Decompressed: 8330
Downloaded: 8378 file(s) [attempted 8378/8546 = 98%, 577 KB/s], Decompressed: 8370
Downloaded: 8418 file(s) [attempted 8418/8546 = 98%, 557 KB/s], Decompressed: 8414
Downloaded: 8465 file(s) [attempted 8465/8546 = 99%, 345 KB/s], Decompressed: 8462
Downloaded: 8512 file(s) [attempted 8512/8546 = 99%, 424 KB/s], Decompressed: 8506
Downloaded: 8545 file(s) [attempted 8545/8546 = 99%, 443 KB/s], Decompressed: 8533
Downloaded: 8546 file(s) [attempted 8546/8546 = 100%, 443 KB/s], Decompressed: 8543

lake build

✔ [3021/3026] Built PrimeNumberTheoremAnd.Fourier (51s)
✔ [3022/3027] Built Architect.Basic (5.7s)
✔ [3023/3027] Built Architect.Command (824ms)
✔ [3024/3027] Built Architect.CollectUsed (873ms)
✔ [3025/3027] Built Architect.Content (887ms)
✔ [3026/3031] Built Architect.Attribute (1.5s)
✔ [3027/3032] Built Architect.Tactic (1.3s)
✔ [3028/3032] Built Architect.Output (1.0s)
✔ [3030/3033] Built Architect.Load (805ms)
✔ [3031/3048] Built Architect (693ms)
✔ [3059/3072] Built PrimeNumberTheoremAnd.Defs (12s)
✔ [3553/3567] Built PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions (10s)
✔ [3566/3588] Built PrimeNumberTheoremAnd.ZetaBounds (19s)
ℹ [3627/3636] Built PrimeNumberTheoremAnd.MediumPNT (32s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3638/3654] Built PrimeNumberTheoremAnd.Backlund.ZeroCountCrude (26s)
⚠ [3651/3656] Built PrimeNumberTheoremAnd.StrongPNT (13s)
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:2041:48: This simp argument is unused:
  neg_div

Hint: Omit it from the simp argument list.
  simp only ̵[̵n̵e̵g̵_̵d̵i̵v̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3654/3656] Built PrimeNumberTheoremAnd.BorelCaratheodory (3.9s)
✔ [3777/3784] Built LeanCert.Core.Interval (2.2s)
✔ [3779/3784] Built LeanCert.Core.IntervalRat.Basic (5.1s)
⚠ [3780/3784] Built PrimeNumberTheoremAnd.Wiener (28s)
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:1392:37: This simp argument is unused:
  show 2 + n - 1 = n + 1 from by omega

Hint: Omit it from the simp argument list.
  simp only [cumsum_succ, show 2 + n - 1 =̵ ̵n̵ ̵+̵ ̵1̵ ̵f̵r̵o̵m̵ ̵b̵y̵ ̵o̵m̵e̵g̵a̵,̵
  ̵ ̵ ̵ ̵ ̵ ̵ ̵s̵h̵o̵w̵ ̵2̵ ̵+̵ ̵n̵ ̵- 1 -̵ ̵1̵ ̵= n from by omega,
  ̲  ̲ ̲ ̲show 2 + n = n + 2 from by omega, show 1 + n = n + 1 from by omega]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Wiener.lean:1393:6: This simp argument is unused:
  show 2 + n - 1 - 1 = n from by omega

Hint: Omit it from the simp argument list.
  simp only [cumsum_succ, show 2 + n - 1 = n + 1 from by omega,
      show 2 + n -̵ ̵1̵ ̵-̵ ̵1̵ ̵= n f̵r̵o̵m̵ ̵b̵y̵ ̵o̵m̵e̵g̵a̵,̵ ̵s̵h̵o̵w̵ ̵2̵ ̵+ n̵ ̵=̵ ̵n̵ ̵+̵ ̵2 from by omega, show 1 + n = n + 1 from by omega]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Wiener.lean:1393:44: This simp argument is unused:
  show 2 + n = n + 2 from by omega

Hint: Omit it from the simp argument list.
  simp only [cumsum_succ, show 2 + n - 1 = n + 1 from by omega,
      show 2 + n - 1 - 1 = n from by omega, show 2̵ ̵+̵ ̵n̵ ̵=̵ ̵n̵ ̵+̵ ̵2̵ ̵f̵r̵o̵m̵ ̵b̵y̵ ̵o̵m̵e̵g̵a̵,̵
  ̵ ̵ ̵ ̵ ̵ ̵ ̵s̵h̵o̵w̵ ̵1 + n = n + 1 from by omega]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Wiener.lean:1394:6: This simp argument is unused:
  show 1 + n = n + 1 from by omega

Hint: Omit it from the simp argument list.
  simp only [cumsum_succ, show 2 + n - 1 = n + 1 from by omega,
      show 2 + n - 1 - 1 = n from by omega, show 2 + n = n + 2 from by o̵m̵e̵g̵a̵,̵
  ̵ ̵ ̵ ̵ ̵ ̵ ̵s̵h̵o̵w̵ ̵1̵ ̵+̵ ̵n̵ ̵=̵ ̵n̵ ̵+̵ ̵1̵ ̵f̵r̵o̵m̵ ̵b̵y̵ ̵omega]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [3781/3784] Built LeanCert.Tactic.IntervalAuto.Types (7.7s)
⚠ [3782/3784] Built PrimeNumberTheoremAnd.Consequences (30s)
warning: PrimeNumberTheoremAnd/Consequences.lean:113:77: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [ne_eq, cast_eq_zero, floor_eq_zero, not_lt, mem_atTop_sets, g̵e̵_̵i̵f̵f̵_̵l̵e̵,̵
  ̵ ̵ ̵ ̵ ̵ ̵ ̵ ̵ ̵Set.mem_setOf_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:121:69: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [Pi.sub_apply, neg_sub, norm_eq_abs, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:180:42: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [one_mul, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:242:71: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [Pi.sub_apply, norm_eq_abs, mul_assoc, eventually_atTop, g̵e̵_̵i̵f̵f̵_̵l̵e̵,̵ ̵norm_mul, abs_of_pos hε,
  ̲  ̲ ̲ ̲ ̲ ̲f] at H ⊢

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:254:71: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [isLittleO_iff, norm_eq_abs, norm_mul, eventually_atTop, g̵e̵_̵i̵f̵f̵_̵l̵e̵,̵
  ̵ ̵ ̵ ̵ ̵ ̵ ̵norm_div] at hf1 ⊢

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1014:49: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [EventuallyEq, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1131:12: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [one_div, gt_iff_lt, inv_pos, ofNat_pos, div_one, norm_eq_abs, eventually_atTop,
              g̵e̵_̵i̵ff̵_̵l̵e̵,̵ ̵f̵orall_const] at k_o1

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1211:44: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [norm_eq_abs, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵] at f_small

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1242:44: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [norm_eq_abs, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵] at f_small

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1269:15: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [g̵e̵_̵i̵f̵f̵_̵l̵e̵,̵ ̵a] at hb

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1280:42: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [gt_iff_lt, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵] at first_term

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1282:31: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1309:59: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [_root_.add_lt_add_iff_left, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵] at first_term

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1311:42: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [gt_iff_lt, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1344:48: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [Set.mem_Ioi, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1378:33: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵] at first_helper

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1379:44: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [gt_iff_lt, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵] at second_helper

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1395:15: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [g̵e̵_̵i̵f̵f̵_̵l̵e̵,̵ ̵sup_le_iff] at hb

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1559:44: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [Set.mem_Ici, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵] at squeeze

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [3783/3794] Built LeanCert.Tactic.IntervalAuto.Norm (7.1s)
✔ [3788/3794] Built LeanCert.Core.Expr (3.7s)
✔ [3789/3795] Built LeanCert.Meta.Numeral (2.0s)
✔ [3790/3795] Built LeanCert.Meta.ToExpr (3.7s)
✔ [3791/3795] Built LeanCert.Tactic.IntervalAuto.Extract (2.5s)
✔ [3792/3795] Built LeanCert.Core.Support (2.3s)
✔ [3793/3795] Built LeanCert.Tactic.IntervalAuto.Parse (4.2s)
✔ [3794/3796] Built LeanCert.Tactic.IntervalAuto.Diagnostic (2.6s)
✔ [3795/3797] Built LeanCert.Core.IntervalRat.Transcendental (3.2s)
✔ [3796/3797] Built LeanCert.Core.IntervalRat.LogReduction (3.4s)
✔ [3810/3820] Built LeanCert.Core.DerivativeIntervals (2.2s)
✔ [3812/3822] Built LeanCert.Core.TrigReduction (2.6s)
✔ [3813/3822] Built LeanCert.Core.Taylor (4.7s)
✔ [3814/3823] Built LeanCert.Core.IntervalRat.Taylor (9.1s)
✔ [3815/3823] Built LeanCert.Core.IntervalRat.TrigReduced (2.3s)
✔ [3816/3824] Built LeanCert.Core.IntervalReal (2.0s)
✔ [3817/3825] Built LeanCert.Core.IntervalRealEndpoints (3.1s)
✔ [3818/3826] Built LeanCert.Engine.Eval.Core (4.7s)
✔ [3819/3826] Built LeanCert.Engine.Eval.Extended (3.1s)
✔ [3820/3828] Built LeanCert.Tactic.Bound.Lemmas (2.3s)
✔ [3821/3833] Built LeanCert.Engine.IntervalEval (2.1s)
✔ [3822/3833] Built LeanCert.Contrib.Sinc (3.1s)
✔ [3823/3833] Built LeanCert.Engine.AD.Basic (2.1s)
✔ [3824/3833] Built LeanCert.Engine.AD.Transcendental (3.2s)
✔ [3825/3833] Built LeanCert.Engine.AD.Eval (2.2s)
✔ [3826/3833] Built LeanCert.Engine.AD.Correctness (2.8s)
✔ [3827/3833] Built LeanCert.Engine.AD.Computable (2.8s)
✔ [3828/3834] Built LeanCert.Engine.AD.PartialCorrectness (4.8s)
✔ [3829/3834] Built LeanCert.Engine.AD (2.0s)
✔ [3830/3834] Built LeanCert.Engine.TaylorModel.Core (5.0s)
✔ [3831/3834] Built LeanCert.Meta.ProveSupported (3.1s)
✔ [3832/3836] Built LeanCert.Tactic.IntervalAuto.ProveCommon (4.2s)
✔ [3833/3837] Built LeanCert.Tactic.IntervalAuto.Basic (2.4s)
✔ [3835/3837] Built LeanCert.Engine.TaylorModel.ExpLog (4.9s)
✔ [3836/3849] Built LeanCert.Engine.TaylorModel.Trig (6.1s)
✔ [3845/3853] Built LeanCert.Engine.TaylorModel.Special (2.3s)
✔ [3846/3853] Built LeanCert.Engine.Integrate (3.9s)
✔ [3847/3853] Built LeanCert.Engine.TaylorModel.Hyperbolic (6.0s)
✔ [3848/3856] Built LeanCert.Engine.TaylorModel.Integral (2.7s)
✔ [3849/3856] Built LeanCert.Engine.TaylorModel.Functions (2.1s)
✔ [3850/3856] Built LeanCert.Core.Dyadic (2.1s)
✔ [3851/3856] Built LeanCert.Engine.TaylorModel.Expr (3.5s)
✔ [3852/3856] Built LeanCert.Core.IntervalDyadic (5.2s)
✔ [3853/3860] Built LeanCert.Engine.TaylorModel (2.1s)
✔ [3854/3860] Built LeanCert.Engine.IntervalEvalDyadic (3.4s)
✔ [3855/3861] Built LeanCert.Engine.IntervalEvalRefined (2.8s)
✔ [3856/3861] Built LeanCert.Engine.Affine.Basic (4.1s)
✔ [3857/3861] Built LeanCert.Engine.Optimization.Box (2.4s)
✔ [3858/3864] Built LeanCert.Engine.Affine.Nonlinear (3.4s)
✔ [3859/3864] Built LeanCert.Engine.Affine.Transcendental (2.0s)
✔ [3860/3864] Built LeanCert.Engine.Optimize (3.0s)
✔ [3861/3865] Built LeanCert.Engine.IntervalEvalAffine (2.0s)
✔ [3862/3866] Built LeanCert.Engine.Optimization.Gradient (3.6s)
✔ [3863/3866] Built LeanCert.Engine.RootFinding.Basic (3.4s)
✔ [3864/3867] Built LeanCert.Engine.Optimization.Global (10s)
✔ [3865/3868] Built LeanCert.Engine.RootFinding.Bisection (3.4s)
✔ [3866/3870] Built LeanCert.Engine.RootFinding.Newton (3.4s)
✔ [3867/3871] Built LeanCert.Engine.RootFinding.MVTBounds (4.0s)
✔ [3868/3871] Built LeanCert.Engine.RootFinding.Contraction (3.6s)
✔ [3869/3871] Built LeanCert.Meta.ProveContinuous (3.3s)
✔ [3870/3873] Built LeanCert.Engine.RootFinding.Main (2.0s)
✔ [3871/3874] Built LeanCert.Validity.Bounds.Core (2.3s)
✔ [3872/3876] Built LeanCert.Validity.Bounds.WithInv (2.3s)
✔ [3873/3878] Built LeanCert.Validity.Bounds.Smart (2.4s)
✔ [3874/3879] Built LeanCert.Validity.Bounds.Bridge (2.3s)
✔ [3875/3879] Built LeanCert.Validity.Integration (3.6s)
✔ [3876/3881] Built LeanCert.Validity.Bounds.Basic (2.0s)
✔ [3877/3881] Built LeanCert.Validity.DyadicBounds (2.4s)
✔ [3878/3882] Built LeanCert.Validity.Bounds (4.7s)
✔ [3879/3883] Built LeanCert.Engine.Optimization.BoundVerify (2.6s)
✔ [3880/3884] Built LeanCert.Tactic.IntervalAuto.Multivariate (4.1s)
✔ [3881/3884] Built LeanCert.Tactic.IntervalAuto.Bound (20s)
✔ [3882/3885] Built LeanCert.Tactic.IntervalAuto.OptBound (2.9s)
✔ [3883/3886] Built LeanCert.Tactic.IntervalAuto.RootBound (2.0s)
✔ [3884/3889] Built LeanCert.Tactic.IntervalAuto.PointIneq (11s)
✔ [3885/3896] Built LeanCert.Tactic.IntervalAuto.Subdiv (5.0s)
✔ [3886/3899] Built LeanCert.Tactic.IntervalAuto.Adaptive (6.2s)
✔ [3891/3899] Built PrimeNumberTheoremAnd.IEANTN.KLN (6.8s)
⚠ [3892/3899] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta (2.9s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3893/3901] Built LeanCert.Tactic.IntervalAuto (2.9s)
⚠ [3899/3906] Built PrimeNumberTheoremAnd.IEANTN.Mertens (16s)
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:602:22: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [isBigO_iff, norm_eq_abs, norm_one, mul_one, e̵v̵e̵n̵t̵u̵a̵l̵l̵y̵_̵a̵t̵T̵o̵p̵,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]̵e̲v̲e̲n̲t̲u̲a̲l̲l̲y̲_̲a̲t̲T̲o̲p̲]̲

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:904:24: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [isBigO_iff, norm_eq_abs, one_mem, CStarRing.norm_of_mem_unitary, mul_one,
        eventually_atTop, g̵e̵_̵i̵f̵f̵_̵l̵e̵,̵ ̵E₁p]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1305:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1800:24: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [isBigO_iff, norm_eq_abs, one_mem, CStarRing.norm_of_mem_unitary, mul_one,
        eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1951:77: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [one_div, isBigO_iff, norm_eq_abs, norm_inv, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1988:24: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [isBigO_iff, norm_eq_abs, one_mem, CStarRing.norm_of_mem_unitary, mul_one,
        eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:2250:58: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [isBigO_iff, norm_eq_abs, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:2268:77: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [EventuallyEq.iff_eventually, Pi.div_apply, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [3959/3972] Built LeanCert.Engine.TaylorModel.Log1p (7.7s)
✔ [3962/3972] Built LeanCert.Examples.Li2Base (2.9s)
⚠ [3963/3974] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (52s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:747:29: This simp argument is unused:
  _root_.sum_apply

Hint: Omit it from the simp argument list.
  simp only [bernsteinApproximation, smul_eq_mul, ContinuousMap.coe_sum, ContinuousMap.coe_mul,
      ContinuousMap.coe_const, _̵r̵o̵o̵t̵_̵.̵s̵u̵m̵_̵a̵p̵p̵l̵y̵,̵ ̵Pi.mul_apply, Function.const_apply]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:747:47: This simp argument is unused:
  Pi.mul_apply

Hint: Omit it from the simp argument list.
  simp only [bernsteinApproximation, smul_eq_mul, ContinuousMap.coe_sum, ContinuousMap.coe_mul,
      ContinuousMap.coe_const, _root_.sum_apply, P̵i̵.̵m̵u̵l̵_̵a̵p̵p̵l̵y̵,̵ ̵Function.const_apply]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:747:61: This simp argument is unused:
  Function.const_apply

Hint: Omit it from the simp argument list.
  simp only [bernsteinApproximation, smul_eq_mul, ContinuousMap.coe_sum, ContinuousMap.coe_mul,
      ContinuousMap.coe_const, _root_.sum_apply, Pi.mul_apply,̵ ̵F̵u̵n̵c̵t̵i̵o̵n̵.̵c̵o̵n̵s̵t̵_̵a̵p̵p̵l̵y̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:824:13: This simp argument is unused:
  ContinuousMap.coe_sum

Hint: Omit it from the simp argument list.
  simp only [̵C̵o̵n̵t̵i̵n̵u̵o̵u̵s̵M̵a̵p̵.̵c̵o̵e̵_̵s̵u̵m̵,̵ ̵C̵o̵n̵t̵i̵n̵u̵o̵u̵s̵M̵a̵p̵.̵c̵o̵e̵_̵m̵u̵l̵,̵[̲C̲o̲n̲t̲i̲n̲u̲o̲u̲s̲M̲a̲p̲.̲c̲o̲e̲_̲m̲u̲l̲,̲ ContinuousMap.coe_const, Finset.sum_apply, Pi.mul_apply,
  ̲  ̲ ̲ ̲Function.const_apply, mul_comm] at hsum

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:824:36: This simp argument is unused:
  ContinuousMap.coe_mul

Hint: Omit it from the simp argument list.
  simp only [ContinuousMap.coe_sum, C̵o̵n̵t̵i̵n̵u̵o̵u̵s̵M̵a̵p̵.̵c̵o̵e̵_̵m̵u̵l̵,̵ ̵ContinuousMap.coe_const, Finset.sum_apply, Pi.mul_apply,
  ̲  ̲ ̲ ̲Function.const_apply, mul_comm] at hsum

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:824:59: This simp argument is unused:
  ContinuousMap.coe_const

Hint: Omit it from the simp argument list.
  simp only [ContinuousMap.coe_sum, ContinuousMap.coe_mul, C̵o̵n̵t̵i̵n̵u̵o̵u̵s̵M̵a̵p̵.̵c̵o̵e̵_̵c̵o̵n̵s̵t̵,̵Finset.sum_apply, Pi.mul_apply,
  ̲  ̲ ̲ ̲Function.const_apply, mul_comm] at hsum

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2572: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:2573:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2594: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:2595:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2812: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:2813:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2828: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:2829:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2958: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:2959:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3064: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:3065:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3079: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:3079:4: Try this:
  [apply] simp only [_root_.deriv_ofReal]
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3080:4: `fun_prop` uses `⊢`!
⚠ [3965/3974] Built LeanCert.Examples.Li2Bounds (16s)
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [3966/3975] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (11s)
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`
✔ [3967/3975] Built PrimeNumberTheoremAnd.IEANTN.LiSeries (8.7s)
✔ [3970/3977] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (3.2s)
✔ [3974/3978] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (8.0s)
⚠ [3975/3982] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (7.6s)
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`
⚠ [4109/4117] Built PrimeNumberTheoremAnd.IEANTN.Buthe (14s)
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`
⚠ [4110/4117] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (20s)
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`
✔ [4111/4117] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (84s)
⚠ [4112/4118] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (31s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
✔ [4113/4118] Built LeanCert.Engine.FinSumDyadic (5.6s)
⚠ [4114/4118] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (42s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1519:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1666:4: 'push_cast at this ⊢' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2185:8: declaration uses `sorry`
✔ [4115/4118] Built LeanCert.Examples.BKLNW_a2_base (14s)
✔ [4116/4122] Built LeanCert.Engine.WitnessSum (2.5s)
✔ [4117/4146] Built LeanCert.Engine.ReflectiveSum (4.2s)
✔ [4118/4147] Built LeanCert.Tactic.VecUtil (2.2s)
✔ [4119/4147] Built LeanCert.Tactic.FinSumExpand (1.4s)
✔ [4121/4147] Built LeanCert.Examples.BKLNW_a2_reflective (92s)
✔ [4122/4150] Built LeanCert.Examples.BKLNW_a2_bounds (3.4s)
✔ [4123/4153] Built LeanCert.Examples.BKLNW_a2_pow2 (2.7s)
✔ [4126/4157] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (27s)
✔ [4129/4160] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core (11s)
ℹ [4130/4160] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (53s)
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.
✔ [4131/4160] Built LeanCert.Engine.Chebyshev.Psi (13s)
✔ [4132/4160] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (17s)
✔ [4133/4160] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (4.5s)
✔ [4134/4162] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85 (29s)
✔ [4135/4162] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc (12s)
✔ [4136/4162] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000 (64s)
✔ [4137/4162] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500 (51s)
✔ [4138/4162] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500 (55s)
✔ [4139/4162] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500 (66s)
✔ [4140/4162] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500 (73s)
✔ [4141/4162] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875 (39s)
✔ [4142/4162] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375 (36s)
✔ [4143/4162] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875 (35s)
✔ [4144/4162] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375 (36s)
✔ [4145/4162] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875 (37s)
✔ [4146/4162] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375 (36s)
✔ [4147/4162] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875 (37s)
✔ [4148/4162] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95 (10s)
✔ [4149/4162] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values (9.7s)
✔ [4150/4164] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next (18s)
⚠ [4151/4164] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (13s)
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2634:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2723: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:3093:4: 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`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3685:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3713:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3725:8: declaration uses `sorry`
✔ [4152/4164] Built LeanCert.Engine.ChebyshevPsi (1.0s)
⚠ [4153/4164] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP (21s)
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`
✔ [4155/4164] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43 (60s)
✔ [4157/4167] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (34s)
⚠ [4158/4167] 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`
✔ [4160/4167] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59 (39s)
✔ [4161/4169] Built LeanCert.Engine.Chebyshev.Theta (5.9s)
⚠ [4162/4169] Built PrimeNumberTheoremAnd.IEANTN.Erdos392 (46s)
warning: PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:3160:6: 'change ((pairProd f.a.toList).length : ℝ) ≤ _' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
✔ [4163/4169] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows (4.8s)
✔ [4165/4169] Built LeanCert.Engine.ChebyshevTheta (1.9s)
✔ [4166/4169] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch (19s)
ℹ [4167/4169] 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.
⚠ [4168/4174] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (58s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:317: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:3753: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:3758: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:3761: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:3763: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:3753: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:3804: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:3807: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:3812: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:3812:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3813: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:3812: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:3812:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3823:4: `unfold μ_num_1` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3824: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:3824: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:3826:6: `exact absurd (this y hy₁) (by norm_num [h]; linarith)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3812: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:3812:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:6: `exact absurd ‹_› (not_le_of_gt hc)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4629:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4656:8: declaration uses `sorry`
✔ [4169/4175] Built LeanCert.Cert.Interval (3.6s)
✔ [4170/4176] Built LeanCert.ANT.Step (8.1s)
✔ [4171/4177] Built LeanCert.ANT.Abel (2.6s)
✔ [4172/4177] Built LeanCert.ANT.Asymp.Env (3.3s)
✔ [4173/4177] Built LeanCert.ANT.Asymp.Hyperbola (2.7s)
✔ [4174/4196] Built LeanCert.ANT.Asymp.Stieltjes (2.5s)
✔ [4175/4196] Built LeanCert.ANT.Asymp.Pointwise (2.6s)
✔ [4176/4196] Built LeanCert.ANT.Asymp.Checkers (2.5s)
✔ [4177/4201] Built LeanCert.Engine.Table (525ms)
✔ [4178/4201] Built LeanCert.ANT.Asymp.Inequality (2.5s)
✔ [4179/4201] Built LeanCert.Validity.AffineBounds (2.8s)
✔ [4182/4201] Built LeanCert.ANT.Asymp (2.2s)
✔ [4183/4201] Built LeanCert.Validity.AffineCover (2.2s)
✔ [4184/4202] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore (22s)
✔ [4185/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13 (14s)
✔ [4186/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12 (22s)
✔ [4187/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11 (22s)
✔ [4188/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10 (22s)
✔ [4189/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09 (22s)
✔ [4190/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08 (22s)
✔ [4191/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07 (22s)
✔ [4192/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06 (22s)
✔ [4193/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05 (22s)
✔ [4194/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04 (22s)
✔ [4195/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03 (22s)
✔ [4196/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02 (22s)
✔ [4197/4203] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01 (21s)
✔ [4198/4204] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00 (22s)
⚠ [4201/4205] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext (4.4s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4203/4206] Built PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor (7.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`
⚠ [4214/4225] Built PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting (11s)
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2061: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`
✖ [4219/4225] Building PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers (5.8s)
trace: .> LEAN_PATH=/apx/source/.lake/packages/Cli/.lake/build/lib/lean:/apx/source/.lake/packages/batteries/.lake/build/lib/lean:/apx/source/.lake/packages/Qq/.lake/build/lib/lean:/apx/source/.lake/packages/aesop/.lake/build/lib/lean:/apx/source/.lake/packages/proofwidgets/.lake/build/lib/lean:/apx/source/.lake/packages/importGraph/.lake/build/lib/lean:/apx/source/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/apx/source/.lake/packages/plausible/.lake/build/lib/lean:/apx/source/.lake/packages/LeanArchitect/.lake/build/lib/lean:/apx/source/.lake/packages/checkdecls/.lake/build/lib/lean:/apx/source/.lake/packages/leancert/.lake/build/lib/lean:/apx/source/.lake/packages/PrimeCert/.lake/build/lib/lean:/apx/source/.lake/packages/mathlib/.lake/build/lib/lean:/apx/source/.lake/build/lib/lean /apx/elan/toolchains/leanprover--lean4---v4.31.0/bin/lean /apx/source/PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean -o /apx/source/.lake/build/lib/lean/PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.olean -i /apx/source/.lake/build/lib/lean/PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.ilean -c /apx/source/.lake/build/ir/PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.c --setup /apx/source/.lake/build/ir/PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.setup.json --json
error: PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:39:4: Type mismatch: After simplification, term
  HasDerivAt.comp z₀ (hasDerivAt_zpow n (z₀ - x) (Or.inl hz₀x)) (HasDerivAt.sub_const x (hasDerivAt_id z₀))
 has type
  @HasDerivAt ℂ DenselyNormedField.toNontriviallyNormedField ℂ NormedField.toNormedCommRing.toAddCommGroup
    (NormedAlgebra.toNormedSpace ℂ).toModule PseudoMetricSpace.toUniformSpace.toTopologicalSpace ⋯
    ((fun x ↦ x ^ n) ∘ fun x_1 ↦ x_1 - x) (↑n * (z₀ - x) ^ (n - 1)) z₀
but is expected to have type
  @HasDerivAt ℂ DenselyNormedField.toNontriviallyNormedField ℂ addCommGroup Semiring.toModule
    PseudoMetricSpace.toUniformSpace.toTopologicalSpace ⋯ (fun z ↦ (z - x) ^ n) (↑n * (z₀ - x) ^ (n - 1)) z₀
error: PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:223:63: unsolved goals
case e'_2
φ : ℝ → ℂ
b σ : ℝ
hφ : Continuous φ
hφ_decay : (fun x ↦ φ x * cexp (↑x / 2)) =O[cocompact ℝ] fun x ↦ Real.exp (-(1 / 2 + b) * |x|)
hσ_top : -(1 + b) < σ
hσ_bot : σ < b
h_loc : LocallyIntegrable (fun y ↦ φ y * cexp (-↑σ * ↑y)) volume
hbig_top : (fun y ↦ φ y * cexp (-↑σ * ↑y)) =O[atTop] fun y ↦ Real.exp (-(1 + b + σ) * y)
hbig_bot : (fun y ↦ φ y * cexp (-↑σ * ↑y)) =O[atBot] fun y ↦ Real.exp ((b - σ) * y)
hint_top : IntegrableAtFilter (fun y ↦ Real.exp (-(1 + b + σ) * y)) atTop volume
hα : 0 < b - σ
h_top : IntegrableAtFilter (fun y ↦ Real.exp (-((b - σ) * y))) atTop volume
⊢ Measure.comap Neg.neg volume = Measure.comap Neg.neg ?m.1187

case e'_3
φ : ℝ → ℂ
b σ : ℝ
hφ : Continuous φ
hφ_decay : (fun x ↦ φ x * cexp (↑x / 2)) =O[cocompact ℝ] fun x ↦ Real.exp (-(1 / 2 + b) * |x|)
hσ_top : -(1 + b) < σ
hσ_bot : σ < b
h_loc : LocallyIntegrable (fun y ↦ φ y * cexp (-↑σ * ↑y)) volume
hbig_top : (fun y ↦ φ y * cexp (-↑σ * ↑y)) =O[atTop] fun y ↦ Real.exp (-(1 + b + σ) * y)
hbig_bot : (fun y ↦ φ y * cexp (-↑σ * ↑y)) =O[atBot] fun y ↦ Real.exp ((b - σ) * y)
hint_top : IntegrableAtFilter (fun y ↦ Real.exp (-(1 + b + σ) * y)) atTop volume
hα : 0 < b - σ
h_top : IntegrableAtFilter (fun y ↦ Real.exp (-((b - σ) * y))) atTop volume
⊢ volume = Measure.map ⇑(MeasurableEquiv.neg ℝ).symm ?m.1187

φ : ℝ → ℂ
b σ : ℝ
hφ : Continuous φ
hφ_decay : (fun x ↦ φ x * cexp (↑x / 2)) =O[cocompact ℝ] fun x ↦ Real.exp (-(1 / 2 + b) * |x|)
hσ_top : -(1 + b) < σ
hσ_bot : σ < b
h_loc : LocallyIntegrable (fun y ↦ φ y * cexp (-↑σ * ↑y)) volume
hbig_top : (fun y ↦ φ y * cexp (-↑σ * ↑y)) =O[atTop] fun y ↦ Real.exp (-(1 + b + σ) * y)
hbig_bot : (fun y ↦ φ y * cexp (-↑σ * ↑y)) =O[atBot] fun y ↦ Real.exp ((b - σ) * y)
hint_top : IntegrableAtFilter (fun y ↦ Real.exp (-(1 + b + σ) * y)) atTop volume
hα : 0 < b - σ
h_top : IntegrableAtFilter (fun y ↦ Real.exp (-((b - σ) * y))) atTop volume
⊢ Measure ℝ
error: PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:312:24: `ring_nf` made no progress on the goal
error: Lean exited with code 1
✔ [4220/4259] Built PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative (3.2s)
✔ [4221/4261] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (9.4s)
⚠ [4239/4276] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (13s)
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:93:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:104:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:117:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:154:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:179:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:187:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:195:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:341:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:470:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:564:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:573:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:591:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:600:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:616:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:625:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:678:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:687:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:696:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:756:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:767:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:778:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:788:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:805:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:814:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:937:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:957:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:987:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1013:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1027:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1035:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1050:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1065:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1074:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1089:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1107:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1119:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1136:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1183:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1254:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1306:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1334:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1369:8: declaration uses `sorry`
⚠ [4246/4276] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (9.6s)
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:214:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:338:8: declaration uses `sorry`
⚠ [4252/4283] 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`
✔ [4256/4283] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (11s)
✔ [4258/4283] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (56s)
⚠ [4259/4283] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (11s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [4261/4283] Built PrimeNumberTheoremAnd.LaplaceInversion (9.7s)
warning: PrimeNumberTheoremAnd/LaplaceInversion.lean:1750:4: 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`
warning: PrimeNumberTheoremAnd/LaplaceInversion.lean:1987: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`
warning: PrimeNumberTheoremAnd/LaplaceInversion.lean:1992: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`
warning: PrimeNumberTheoremAnd/LaplaceInversion.lean:2000:8: 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`
✔ [4262/4283] Built PrimeNumberTheoremAnd.IEANTN.Lcm (29s)
⚠ [4265/4283] Built PrimeNumberTheoremAnd.PerronFormula (6.6s)
warning: PrimeNumberTheoremAnd/PerronFormula.lean:138:22: `Set.diff_subset_diff` has been deprecated: Use `Set.sdiff_subset_sdiff` instead
warning: PrimeNumberTheoremAnd/PerronFormula.lean:660:4: 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`
✔ [4267/4283] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (2.7s)
✔ [4280/4283] Built PrimeNumberTheoremAnd.IEANTN.KadiriEq13 (5.2s)
Some required targets logged failures:
- PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers

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

lake build :blueprint

✔ [17/35] Built Architect.Basic:c.o (2.4s)
✔ [18/35] Built Architect.Command:c.o (270ms)
✔ [19/35] Built Architect.Content:c.o (223ms)
✔ [20/35] Built Architect.Attribute:c.o (983ms)
✔ [21/35] Built Architect.CollectUsed:c.o (188ms)
✔ [22/35] Built Architect.Tactic:c.o (780ms)
✔ [23/35] Built Architect.Output:c.o (2.3s)
✔ [24/35] Built Architect.Load:c.o (183ms)
✔ [25/35] Built Architect:c.o (103ms)
✔ [27/35] Built Cli.Basic:c.o (3.2s)
✔ [30/35] Built Cli.Extensions:c.o (496ms)
✔ [31/35] Built Cli:c.o (74ms)
✔ [32/35] Built Main (1.4s)
✔ [33/35] Built Main:c.o (256ms)
✔ [34/41] Built extract_blueprint:exe (5.9s)
✔ [3055/3058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Fourier:blueprint (14s)
✔ [3084/3097] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Defs:blueprint (17s)
✔ [3586/3602] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions:blueprint (16s)
✔ [3601/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (66s)
ℹ [3682/3699] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3687/3701] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (60s)
✔ [3704/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Backlund.ZeroCountCrude:blueprint (3.9s)
⚠ [3708/3727] 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:2041:48: This simp argument is unused:
  neg_div

Hint: Omit it from the simp argument list.
  simp only ̵[̵n̵e̵g̵_̵d̵i̵v̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3719/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (49s)
✔ [3723/3734] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (6.9s)
⚠ [3848/3857] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:1392:37: This simp argument is unused:
  show 2 + n - 1 = n + 1 from by omega

Hint: Omit it from the simp argument list.
  simp only [cumsum_succ, show 2 + n - 1 =̵ ̵n̵ ̵+̵ ̵1̵ ̵f̵r̵o̵m̵ ̵b̵y̵ ̵o̵m̵e̵g̵a̵,̵
  ̵ ̵ ̵ ̵ ̵ ̵ ̵s̵h̵o̵w̵ ̵2̵ ̵+̵ ̵n̵ ̵- 1 -̵ ̵1̵ ̵= n from by omega,
  ̲  ̲ ̲ ̲show 2 + n = n + 2 from by omega, show 1 + n = n + 1 from by omega]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Wiener.lean:1393:6: This simp argument is unused:
  show 2 + n - 1 - 1 = n from by omega

Hint: Omit it from the simp argument list.
  simp only [cumsum_succ, show 2 + n - 1 = n + 1 from by omega,
      show 2 + n -̵ ̵1̵ ̵-̵ ̵1̵ ̵= n f̵r̵o̵m̵ ̵b̵y̵ ̵o̵m̵e̵g̵a̵,̵ ̵s̵h̵o̵w̵ ̵2̵ ̵+ n̵ ̵=̵ ̵n̵ ̵+̵ ̵2 from by omega, show 1 + n = n + 1 from by omega]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Wiener.lean:1393:44: This simp argument is unused:
  show 2 + n = n + 2 from by omega

Hint: Omit it from the simp argument list.
  simp only [cumsum_succ, show 2 + n - 1 = n + 1 from by omega,
      show 2 + n - 1 - 1 = n from by omega, show 2̵ ̵+̵ ̵n̵ ̵=̵ ̵n̵ ̵+̵ ̵2̵ ̵f̵r̵o̵m̵ ̵b̵y̵ ̵o̵m̵e̵g̵a̵,̵
  ̵ ̵ ̵ ̵ ̵ ̵ ̵s̵h̵o̵w̵ ̵1 + n = n + 1 from by omega]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Wiener.lean:1394:6: This simp argument is unused:
  show 1 + n = n + 1 from by omega

Hint: Omit it from the simp argument list.
  simp only [cumsum_succ, show 2 + n - 1 = n + 1 from by omega,
      show 2 + n - 1 - 1 = n from by omega, show 2 + n = n + 2 from by o̵m̵e̵g̵a̵,̵
  ̵ ̵ ̵ ̵ ̵ ̵ ̵s̵h̵o̵w̵ ̵1̵ ̵+̵ ̵n̵ ̵=̵ ̵n̵ ̵+̵ ̵1̵ ̵f̵r̵o̵m̵ ̵b̵y̵ ̵omega]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [3851/3857] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Wiener:blueprint (39s)
⚠ [3852/3857] Replayed PrimeNumberTheoremAnd.Consequences
warning: PrimeNumberTheoremAnd/Consequences.lean:113:77: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [ne_eq, cast_eq_zero, floor_eq_zero, not_lt, mem_atTop_sets, g̵e̵_̵i̵f̵f̵_̵l̵e̵,̵
  ̵ ̵ ̵ ̵ ̵ ̵ ̵ ̵ ̵Set.mem_setOf_eq]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:121:69: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [Pi.sub_apply, neg_sub, norm_eq_abs, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:180:42: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [one_mul, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:242:71: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [Pi.sub_apply, norm_eq_abs, mul_assoc, eventually_atTop, g̵e̵_̵i̵f̵f̵_̵l̵e̵,̵ ̵norm_mul, abs_of_pos hε,
  ̲  ̲ ̲ ̲ ̲ ̲f] at H ⊢

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:254:71: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [isLittleO_iff, norm_eq_abs, norm_mul, eventually_atTop, g̵e̵_̵i̵f̵f̵_̵l̵e̵,̵
  ̵ ̵ ̵ ̵ ̵ ̵ ̵norm_div] at hf1 ⊢

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1014:49: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [EventuallyEq, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1131:12: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [one_div, gt_iff_lt, inv_pos, ofNat_pos, div_one, norm_eq_abs, eventually_atTop,
              g̵e̵_̵i̵ff̵_̵l̵e̵,̵ ̵f̵orall_const] at k_o1

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1211:44: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [norm_eq_abs, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵] at f_small

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1242:44: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [norm_eq_abs, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵] at f_small

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1269:15: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [g̵e̵_̵i̵f̵f̵_̵l̵e̵,̵ ̵a] at hb

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1280:42: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [gt_iff_lt, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵] at first_term

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1282:31: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1309:59: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [_root_.add_lt_add_iff_left, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵] at first_term

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1311:42: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [gt_iff_lt, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1344:48: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [Set.mem_Ioi, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1378:33: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵] at first_helper

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1379:44: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [gt_iff_lt, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵] at second_helper

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1395:15: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [g̵e̵_̵i̵f̵f̵_̵l̵e̵,̵ ̵sup_le_iff] at hb

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/Consequences.lean:1559:44: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [Set.mem_Ici, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵] at squeeze

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [3855/3878] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Consequences:blueprint (14s)
⚠ [3966/3982] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3973/3984] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KLN:blueprint (3.2s)
✔ [3974/3984] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta:blueprint (3.3s)
⚠ [3976/3984] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:602:22: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [isBigO_iff, norm_eq_abs, norm_one, mul_one, e̵v̵e̵n̵t̵u̵a̵l̵l̵y̵_̵a̵t̵T̵o̵p̵,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]̵e̲v̲e̲n̲t̲u̲a̲l̲l̲y̲_̲a̲t̲T̲o̲p̲]̲

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:904:24: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [isBigO_iff, norm_eq_abs, one_mem, CStarRing.norm_of_mem_unitary, mul_one,
        eventually_atTop, g̵e̵_̵i̵f̵f̵_̵l̵e̵,̵ ̵E₁p]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1305:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1800:24: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [isBigO_iff, norm_eq_abs, one_mem, CStarRing.norm_of_mem_unitary, mul_one,
        eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1951:77: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [one_div, isBigO_iff, norm_eq_abs, norm_inv, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1988:24: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [isBigO_iff, norm_eq_abs, one_mem, CStarRing.norm_of_mem_unitary, mul_one,
        eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:2250:58: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [isBigO_iff, norm_eq_abs, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:2268:77: This simp argument is unused:
  ge_iff_le

Hint: Omit it from the simp argument list.
  simp only [EventuallyEq.iff_eventually, Pi.div_apply, eventually_atTop,̵ ̵g̵e̵_̵i̵f̵f̵_̵l̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [3982/3992] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (45s)
⚠ [4046/4067] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:747:29: This simp argument is unused:
  _root_.sum_apply

Hint: Omit it from the simp argument list.
  simp only [bernsteinApproximation, smul_eq_mul, ContinuousMap.coe_sum, ContinuousMap.coe_mul,
      ContinuousMap.coe_const, _̵r̵o̵o̵t̵_̵.̵s̵u̵m̵_̵a̵p̵p̵l̵y̵,̵ ̵Pi.mul_apply, Function.const_apply]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:747:47: This simp argument is unused:
  Pi.mul_apply

Hint: Omit it from the simp argument list.
  simp only [bernsteinApproximation, smul_eq_mul, ContinuousMap.coe_sum, ContinuousMap.coe_mul,
      ContinuousMap.coe_const, _root_.sum_apply, P̵i̵.̵m̵u̵l̵_̵a̵p̵p̵l̵y̵,̵ ̵Function.const_apply]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:747:61: This simp argument is unused:
  Function.const_apply

Hint: Omit it from the simp argument list.
  simp only [bernsteinApproximation, smul_eq_mul, ContinuousMap.coe_sum, ContinuousMap.coe_mul,
      ContinuousMap.coe_const, _root_.sum_apply, Pi.mul_apply,̵ ̵F̵u̵n̵c̵t̵i̵o̵n̵.̵c̵o̵n̵s̵t̵_̵a̵p̵p̵l̵y̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:824:13: This simp argument is unused:
  ContinuousMap.coe_sum

Hint: Omit it from the simp argument list.
  simp only [̵C̵o̵n̵t̵i̵n̵u̵o̵u̵s̵M̵a̵p̵.̵c̵o̵e̵_̵s̵u̵m̵,̵ ̵C̵o̵n̵t̵i̵n̵u̵o̵u̵s̵M̵a̵p̵.̵c̵o̵e̵_̵m̵u̵l̵,̵[̲C̲o̲n̲t̲i̲n̲u̲o̲u̲s̲M̲a̲p̲.̲c̲o̲e̲_̲m̲u̲l̲,̲ ContinuousMap.coe_const, Finset.sum_apply, Pi.mul_apply,
  ̲  ̲ ̲ ̲Function.const_apply, mul_comm] at hsum

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:824:36: This simp argument is unused:
  ContinuousMap.coe_mul

Hint: Omit it from the simp argument list.
  simp only [ContinuousMap.coe_sum, C̵o̵n̵t̵i̵n̵u̵o̵u̵s̵M̵a̵p̵.̵c̵o̵e̵_̵m̵u̵l̵,̵ ̵ContinuousMap.coe_const, Finset.sum_apply, Pi.mul_apply,
  ̲  ̲ ̲ ̲Function.const_apply, mul_comm] at hsum

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:824:59: This simp argument is unused:
  ContinuousMap.coe_const

Hint: Omit it from the simp argument list.
  simp only [ContinuousMap.coe_sum, ContinuousMap.coe_mul, C̵o̵n̵t̵i̵n̵u̵o̵u̵s̵M̵a̵p̵.̵c̵o̵e̵_̵c̵o̵n̵s̵t̵,̵Finset.sum_apply, Pi.mul_apply,
  ̲  ̲ ̲ ̲Function.const_apply, mul_comm] at hsum

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2572: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:2573:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2594: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:2595:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2812: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:2813:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2828: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:2829:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2958: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:2959:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3064: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:3065:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3079: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:3079:4: Try this:
  [apply] simp only [_root_.deriv_ofReal]
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3080:4: `fun_prop` uses `⊢`!
⚠ [4047/4067] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [4053/4068] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (27s)
⚠ [4054/4068] 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`
✔ [4057/4070] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaSummary:blueprint (3.0s)
✔ [4060/4070] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LiSeries:blueprint (3.1s)
✔ [4064/4070] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (3.5s)
⚠ [4065/4070] 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`
✔ [4068/4074] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (16s)
✔ [4069/4074] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (11s)
⚠ [4198/4213] 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`
⚠ [4202/4217] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
✔ [4205/4217] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (6.9s)
⚠ [4206/4217] 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`
✔ [4210/4269] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (25s)
✔ [4211/4269] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (21s)
✔ [4212/4269] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (5.3s)
⚠ [4213/4269] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1519:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1666:4: 'push_cast at this ⊢' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2185:8: declaration uses `sorry`
✔ [4216/4269] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (24s)
✔ [4227/4289] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (5.5s)
ℹ [4230/4289] 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.
✔ [4231/4291] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core:blueprint (3.7s)
✔ [4252/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next:blueprint (3.6s)
✔ [4253/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values:blueprint (3.6s)
✔ [4255/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85:blueprint (3.6s)
✔ [4256/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95:blueprint (3.6s)
✔ [4257/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875:blueprint (3.7s)
✔ [4258/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375:blueprint (3.8s)
✔ [4259/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875:blueprint (3.8s)
✔ [4260/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375:blueprint (3.8s)
✔ [4261/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875:blueprint (3.6s)
✔ [4262/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375:blueprint (3.7s)
✔ [4263/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875:blueprint (3.7s)
✔ [4264/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500:blueprint (3.7s)
✔ [4265/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500:blueprint (3.8s)
✔ [4266/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500:blueprint (3.7s)
✔ [4267/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500:blueprint (3.7s)
✔ [4268/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000:blueprint (3.6s)
✔ [4269/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc:blueprint (3.6s)
✔ [4270/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (51s)
⚠ [4271/4294] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2634:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2723: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:3093:4: 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`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3685:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3713:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3725:8: declaration uses `sorry`
✔ [4273/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (4.8s)
✔ [4274/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables:blueprint (2.0s)
⚠ [4275/4294] 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`
✔ [4278/4301] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43:blueprint (3.9s)
✔ [4280/4301] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (20s)
✔ [4282/4301] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP:blueprint (3.9s)
⚠ [4283/4301] 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`
✔ [4286/4301] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59:blueprint (3.7s)
✔ [4288/4301] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (18s)
✔ [4289/4301] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (19s)
⚠ [4290/4301] Replayed PrimeNumberTheoremAnd.IEANTN.Erdos392
warning: PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:3160:6: 'change ((pairProd f.a.toList).length : ℝ) ≤ _' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
✔ [4293/4305] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows:blueprint (3.5s)
✔ [4295/4305] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (17s)
ℹ [4296/4305] 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.
✔ [4297/4307] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch:blueprint (12s)
✔ [4298/4307] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations:blueprint (8.2s)
⚠ [4299/4307] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:317: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:3753: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:3758: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:3761: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:3763: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:3753: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:3804: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:3807: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:3812: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:3812:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3813: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:3812: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:3812:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3823:4: `unfold μ_num_1` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3824: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:3824: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:3826:6: `exact absurd (this y hy₁) (by norm_num [h]; linarith)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3812: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:3812:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:6: `exact absurd ‹_› (not_le_of_gt hc)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4629:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4656:8: declaration uses `sorry`
✔ [4301/4309] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (32s)
✔ [4318/4354] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore:blueprint (3.5s)
✔ [4335/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00:blueprint (3.4s)
✔ [4336/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01:blueprint (3.5s)
✔ [4337/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02:blueprint (3.4s)
✔ [4338/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03:blueprint (3.6s)
✔ [4339/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04:blueprint (3.5s)
✔ [4340/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05:blueprint (3.5s)
✔ [4341/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06:blueprint (3.4s)
✔ [4342/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07:blueprint (3.6s)
✔ [4343/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08:blueprint (3.5s)
✔ [4344/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09:blueprint (3.5s)
✔ [4345/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10:blueprint (3.5s)
✔ [4346/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11:blueprint (3.5s)
✔ [4347/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12:blueprint (3.4s)
✔ [4348/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13:blueprint (3.5s)
⚠ [4349/4356] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
✔ [4351/4359] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext:blueprint (3.4s)
⚠ [4352/4359] 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`
✔ [4355/4384] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor:blueprint (5.6s)
⚠ [4363/4384] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2061: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`
✔ [4365/4384] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting:blueprint (3.6s)
✖ [4370/4449] Building PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers (8.2s)
trace: .> LEAN_PATH=/apx/source/.lake/packages/Cli/.lake/build/lib/lean:/apx/source/.lake/packages/batteries/.lake/build/lib/lean:/apx/source/.lake/packages/Qq/.lake/build/lib/lean:/apx/source/.lake/packages/aesop/.lake/build/lib/lean:/apx/source/.lake/packages/proofwidgets/.lake/build/lib/lean:/apx/source/.lake/packages/importGraph/.lake/build/lib/lean:/apx/source/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/apx/source/.lake/packages/plausible/.lake/build/lib/lean:/apx/source/.lake/packages/LeanArchitect/.lake/build/lib/lean:/apx/source/.lake/packages/checkdecls/.lake/build/lib/lean:/apx/source/.lake/packages/leancert/.lake/build/lib/lean:/apx/source/.lake/packages/PrimeCert/.lake/build/lib/lean:/apx/source/.lake/packages/mathlib/.lake/build/lib/lean:/apx/source/.lake/build/lib/lean /apx/elan/toolchains/leanprover--lean4---v4.31.0/bin/lean /apx/source/PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean -o /apx/source/.lake/build/lib/lean/PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.olean -i /apx/source/.lake/build/lib/lean/PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.ilean -c /apx/source/.lake/build/ir/PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.c --setup /apx/source/.lake/build/ir/PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.setup.json --json
error: PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:39:4: Type mismatch: After simplification, term
  HasDerivAt.comp z₀ (hasDerivAt_zpow n (z₀ - x) (Or.inl hz₀x)) (HasDerivAt.sub_const x (hasDerivAt_id z₀))
 has type
  @HasDerivAt ℂ DenselyNormedField.toNontriviallyNormedField ℂ NormedField.toNormedCommRing.toAddCommGroup
    (NormedAlgebra.toNormedSpace ℂ).toModule PseudoMetricSpace.toUniformSpace.toTopologicalSpace ⋯
    ((fun x ↦ x ^ n) ∘ fun x_1 ↦ x_1 - x) (↑n * (z₀ - x) ^ (n - 1)) z₀
but is expected to have type
  @HasDerivAt ℂ DenselyNormedField.toNontriviallyNormedField ℂ addCommGroup Semiring.toModule
    PseudoMetricSpace.toUniformSpace.toTopologicalSpace ⋯ (fun z ↦ (z - x) ^ n) (↑n * (z₀ - x) ^ (n - 1)) z₀
error: PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:223:63: unsolved goals
case e'_2
φ : ℝ → ℂ
b σ : ℝ
hφ : Continuous φ
hφ_decay : (fun x ↦ φ x * cexp (↑x / 2)) =O[cocompact ℝ] fun x ↦ Real.exp (-(1 / 2 + b) * |x|)
hσ_top : -(1 + b) < σ
hσ_bot : σ < b
h_loc : LocallyIntegrable (fun y ↦ φ y * cexp (-↑σ * ↑y)) volume
hbig_top : (fun y ↦ φ y * cexp (-↑σ * ↑y)) =O[atTop] fun y ↦ Real.exp (-(1 + b + σ) * y)
hbig_bot : (fun y ↦ φ y * cexp (-↑σ * ↑y)) =O[atBot] fun y ↦ Real.exp ((b - σ) * y)
hint_top : IntegrableAtFilter (fun y ↦ Real.exp (-(1 + b + σ) * y)) atTop volume
hα : 0 < b - σ
h_top : IntegrableAtFilter (fun y ↦ Real.exp (-((b - σ) * y))) atTop volume
⊢ Measure.comap Neg.neg volume = Measure.comap Neg.neg ?m.1187

case e'_3
φ : ℝ → ℂ
b σ : ℝ
hφ : Continuous φ
hφ_decay : (fun x ↦ φ x * cexp (↑x / 2)) =O[cocompact ℝ] fun x ↦ Real.exp (-(1 / 2 + b) * |x|)
hσ_top : -(1 + b) < σ
hσ_bot : σ < b
h_loc : LocallyIntegrable (fun y ↦ φ y * cexp (-↑σ * ↑y)) volume
hbig_top : (fun y ↦ φ y * cexp (-↑σ * ↑y)) =O[atTop] fun y ↦ Real.exp (-(1 + b + σ) * y)
hbig_bot : (fun y ↦ φ y * cexp (-↑σ * ↑y)) =O[atBot] fun y ↦ Real.exp ((b - σ) * y)
hint_top : IntegrableAtFilter (fun y ↦ Real.exp (-(1 + b + σ) * y)) atTop volume
hα : 0 < b - σ
h_top : IntegrableAtFilter (fun y ↦ Real.exp (-((b - σ) * y))) atTop volume
⊢ volume = Measure.map ⇑(MeasurableEquiv.neg ℝ).symm ?m.1187

φ : ℝ → ℂ
b σ : ℝ
hφ : Continuous φ
hφ_decay : (fun x ↦ φ x * cexp (↑x / 2)) =O[cocompact ℝ] fun x ↦ Real.exp (-(1 / 2 + b) * |x|)
hσ_top : -(1 + b) < σ
hσ_bot : σ < b
h_loc : LocallyIntegrable (fun y ↦ φ y * cexp (-↑σ * ↑y)) volume
hbig_top : (fun y ↦ φ y * cexp (-↑σ * ↑y)) =O[atTop] fun y ↦ Real.exp (-(1 + b + σ) * y)
hbig_bot : (fun y ↦ φ y * cexp (-↑σ * ↑y)) =O[atBot] fun y ↦ Real.exp ((b - σ) * y)
hint_top : IntegrableAtFilter (fun y ↦ Real.exp (-(1 + b + σ) * y)) atTop volume
hα : 0 < b - σ
h_top : IntegrableAtFilter (fun y ↦ Real.exp (-((b - σ) * y))) atTop volume
⊢ Measure ℝ
error: PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:312:24: `ring_nf` made no progress on the goal
error: Lean exited with code 1
✔ [4393/4481] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative:blueprint (17s)
✔ [4394/4481] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (5.4s)
⚠ [4395/4481] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:93:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:104:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:117:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:154:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:179:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:187:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:195:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:341:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:470:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:564:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:573:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:591:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:600:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:616:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:625:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:678:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:687:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:696:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:756:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:767:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:778:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:788:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:805:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:814:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:937:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:957:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:987:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1013:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1027:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1035:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1050:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1065:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1074:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1089:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1107:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1119:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1136:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1183:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1254:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1306:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1334:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1369:8: declaration uses `sorry`
⚠ [4422/4492] 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`
✔ [4424/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (46s)
⚠ [4425/4492] Replayed PrimeNumberTheoremAnd.IEANTN.SecondarySummary
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:214:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:338:8: declaration uses `sorry`
⚠ [4437/4492] Replayed PrimeNumberTheoremAnd.LaplaceInversion
warning: PrimeNumberTheoremAnd/LaplaceInversion.lean:1750:4: 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`
warning: PrimeNumberTheoremAnd/LaplaceInversion.lean:1987: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`
warning: PrimeNumberTheoremAnd/LaplaceInversion.lean:1992: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`
warning: PrimeNumberTheoremAnd/LaplaceInversion.lean:2000:8: 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`
⚠ [4443/4492] Replayed PrimeNumberTheoremAnd.PerronFormula
warning: PrimeNumberTheoremAnd/PerronFormula.lean:138:22: `Set.diff_subset_diff` has been deprecated: Use `Set.sdiff_subset_sdiff` instead
warning: PrimeNumberTheoremAnd/PerronFormula.lean:660:4: 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`
✔ [4444/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (11s)
✔ [4446/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (7.2s)
⚠ [4447/4492] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4455/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.LaplaceInversion:blueprint (2.6s)
✔ [4458/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.PerronFormula:blueprint (22s)
✔ [4459/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (6.4s)
✔ [4467/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (11s)
✔ [4468/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (3.4s)
✔ [4469/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (15s)
✔ [4486/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriEq13:blueprint (5.1s)
Some required targets logged failures:
- PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers

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