Run 90

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

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

git checkout efed0f9ec8f4bceb69f1ca1ae8c8ffa07dced887

Note: switching to 'efed0f9ec8f4bceb69f1ca1ae8c8ffa07dced887'.

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 efed0f9 chore: bump to Lean v4.31.0 and drop upstreamed CostaPereira (#1600)

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)

info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision 'db127794c79fdeb86f6b0cf6ff2c804026fbaff1'
info: PrimeCert: cloning https://github.com/b-mehta/PrimeCert
info: PrimeCert: checking out revision 'f699a3e5d3efb381b9ddfb61a1ca51be25f456bd'
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'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'fc38104235ab6cf8a448a74405aa258804ef4e36'
✔ [1/5] Built Cache.Cli (448ms)
✔ [2/5] Built Cache.Lean (430ms)
✔ [6/11] Built Cache.Infra (503ms)
✔ [7/12] Built Cache.IO (1.6s)
✔ [8/15] Built Cache.Hashing (921ms)
✔ [10/26] Built Cache.Requests (2.0s)
✔ [11/26] Built Cache.Cli:c.o (1.4s)
✔ [12/26] Built Cache.Lean:c.o (136ms)
✔ [14/26] Built Cache.IO:c.o (1.2s)
✔ [15/26] Built Cache.Hashing:c.o (377ms)
✔ [16/26] Built Cache.Infra:c.o (187ms)
✔ [17/26] Built Cache.Requests:c.o (2.0s)
✔ [18/26] Built Cache.Marker (723ms)
✔ [19/26] Built Cache.Marker:c.o (108ms)
✔ [20/26] Built Cache.Query (735ms)
✔ [21/26] Built Cache.Query:c.o (236ms)
✔ [22/26] Built Cache.Warning (775ms)
✔ [23/26] Built Cache.Warning:c.o (213ms)
✔ [24/26] Built Cache.Main (1.6s)
✔ [25/26] Built Cache.Main:c.o (762ms)
✔ [26/26] Built cache:exe (5.8s)

Downloaded: 1 file(s) [attempted 1/8546 = 0%, 13 KB/s], Decompressed: 0
Downloaded: 17 file(s) [attempted 17/8546 = 0%, 29 KB/s], Decompressed: 9
Downloaded: 41 file(s) [attempted 41/8546 = 0%, 12 KB/s], Decompressed: 37
Downloaded: 66 file(s) [attempted 66/8546 = 0%, 33 KB/s], Decompressed: 56
Downloaded: 91 file(s) [attempted 91/8546 = 1%, 462 KB/s], Decompressed: 78
Downloaded: 122 file(s) [attempted 122/8546 = 1%, 287 KB/s], Decompressed: 102
Downloaded: 153 file(s) [attempted 153/8546 = 1%, 285 KB/s], Decompressed: 116
Downloaded: 194 file(s) [attempted 194/8546 = 2%, 269 KB/s], Decompressed: 160
Downloaded: 231 file(s) [attempted 231/8546 = 2%, 377 KB/s], Decompressed: 183
Downloaded: 268 file(s) [attempted 268/8546 = 3%, 275 KB/s], Decompressed: 234
Downloaded: 309 file(s) [attempted 309/8546 = 3%, 25 KB/s], Decompressed: 234
Downloaded: 343 file(s) [attempted 343/8546 = 4%, 121 KB/s], Decompressed: 268
Downloaded: 383 file(s) [attempted 383/8546 = 4%, 82 KB/s], Decompressed: 312
Downloaded: 424 file(s) [attempted 424/8546 = 4%, 96 KB/s], Decompressed: 312
Downloaded: 461 file(s) [attempted 461/8546 = 5%, 217 KB/s], Decompressed: 366
Downloaded: 498 file(s) [attempted 498/8546 = 5%, 435 KB/s], Decompressed: 427
Downloaded: 536 file(s) [attempted 536/8546 = 6%, 553 KB/s], Decompressed: 427
Downloaded: 573 file(s) [attempted 573/8546 = 6%, 447 KB/s], Decompressed: 427
Downloaded: 617 file(s) [attempted 617/8546 = 7%, 216 KB/s], Decompressed: 498
Downloaded: 654 file(s) [attempted 654/8546 = 7%, 911 KB/s], Decompressed: 498
Downloaded: 698 file(s) [attempted 698/8546 = 8%, 701 KB/s], Decompressed: 498
Downloaded: 735 file(s) [attempted 735/8546 = 8%, 78 KB/s], Decompressed: 597
Downloaded: 776 file(s) [attempted 776/8546 = 9%, 874 KB/s], Decompressed: 597
Downloaded: 813 file(s) [attempted 813/8546 = 9%, 300 KB/s], Decompressed: 597
Downloaded: 854 file(s) [attempted 854/8546 = 9%, 95 KB/s], Decompressed: 597
Downloaded: 898 file(s) [attempted 898/8546 = 10%, 1058 KB/s], Decompressed: 722
Downloaded: 938 file(s) [attempted 938/8546 = 10%, 177 KB/s], Decompressed: 722
Downloaded: 986 file(s) [attempted 986/8546 = 11%, 756 KB/s], Decompressed: 722
Downloaded: 1026 file(s) [attempted 1026/8546 = 12%, 578 KB/s], Decompressed: 722
Downloaded: 1064 file(s) [attempted 1064/8546 = 12%, 2118 KB/s], Decompressed: 874
Downloaded: 1104 file(s) [attempted 1104/8546 = 12%, 79 KB/s], Decompressed: 874
Downloaded: 1141 file(s) [attempted 1141/8546 = 13%, 281 KB/s], Decompressed: 874
Downloaded: 1185 file(s) [attempted 1185/8546 = 13%, 894 KB/s], Decompressed: 874
Downloaded: 1229 file(s) [attempted 1229/8546 = 14%, 102 KB/s], Decompressed: 874
Downloaded: 1269 file(s) [attempted 1269/8546 = 14%, 112 KB/s], Decompressed: 874
Downloaded: 1307 file(s) [attempted 1307/8546 = 15%, 443 KB/s], Decompressed: 874
Downloaded: 1344 file(s) [attempted 1344/8546 = 15%, 51 KB/s], Decompressed: 1064
Downloaded: 1378 file(s) [attempted 1378/8546 = 16%, 339 KB/s], Decompressed: 1064
Downloaded: 1422 file(s) [attempted 1422/8546 = 16%, 112 KB/s], Decompressed: 1064
Downloaded: 1459 file(s) [attempted 1459/8546 = 17%, 693 KB/s], Decompressed: 1064
Downloaded: 1500 file(s) [attempted 1500/8546 = 17%, 385 KB/s], Decompressed: 1064
Downloaded: 1537 file(s) [attempted 1537/8546 = 17%, 71 KB/s], Decompressed: 1064
Downloaded: 1574 file(s) [attempted 1574/8546 = 18%, 138 KB/s], Decompressed: 1064
Downloaded: 1618 file(s) [attempted 1618/8546 = 18%, 104 KB/s], Decompressed: 1064
Downloaded: 1659 file(s) [attempted 1659/8546 = 19%, 24 KB/s], Decompressed: 1314
Downloaded: 1703 file(s) [attempted 1703/8546 = 19%, 378 KB/s], Decompressed: 1314
Downloaded: 1740 file(s) [attempted 1740/8546 = 20%, 1908 KB/s], Decompressed: 1314
Downloaded: 1781 file(s) [attempted 1781/8546 = 20%, 170 KB/s], Decompressed: 1314
Downloaded: 1825 file(s) [attempted 1825/8546 = 21%, 61 KB/s], Decompressed: 1314
Downloaded: 1859 file(s) [attempted 1859/8546 = 21%, 1170 KB/s], Decompressed: 1314
Downloaded: 1899 file(s) [attempted 1899/8546 = 22%, 306 KB/s], Decompressed: 1314
Downloaded: 1940 file(s) [attempted 1940/8546 = 22%, 137 KB/s], Decompressed: 1314
Downloaded: 1977 file(s) [attempted 1977/8546 = 23%, 311 KB/s], Decompressed: 1314
Downloaded: 2018 file(s) [attempted 2018/8546 = 23%, 1545 KB/s], Decompressed: 1314
Downloaded: 2051 file(s) [attempted 2051/8546 = 23%, 192 KB/s], Decompressed: 1622
Downloaded: 2099 file(s) [attempted 2099/8546 = 24%, 229 KB/s], Decompressed: 1622
Downloaded: 2143 file(s) [attempted 2143/8546 = 25%, 192 KB/s], Decompressed: 1622
Downloaded: 2183 file(s) [attempted 2183/8546 = 25%, 418 KB/s], Decompressed: 1622
Downloaded: 2231 file(s) [attempted 2231/8546 = 26%, 230 KB/s], Decompressed: 1622
Downloaded: 2265 file(s) [attempted 2265/8546 = 26%, 427 KB/s], Decompressed: 1622
Downloaded: 2305 file(s) [attempted 2305/8546 = 26%, 138 KB/s], Decompressed: 1622
Downloaded: 2352 file(s) [attempted 2352/8546 = 27%, 500 KB/s], Decompressed: 1622
Downloaded: 2396 file(s) [attempted 2396/8546 = 28%, 304 KB/s], Decompressed: 1622
Downloaded: 2437 file(s) [attempted 2437/8546 = 28%, 44 KB/s], Decompressed: 1622
Downloaded: 2481 file(s) [attempted 2481/8546 = 29%, 462 KB/s], Decompressed: 1622
Downloaded: 2522 file(s) [attempted 2522/8546 = 29%, 334 KB/s], Decompressed: 1622
Downloaded: 2559 file(s) [attempted 2559/8546 = 29%, 312 KB/s], Decompressed: 2028
Downloaded: 2596 file(s) [attempted 2596/8546 = 30%, 102 KB/s], Decompressed: 2028
Downloaded: 2640 file(s) [attempted 2640/8546 = 30%, 23 KB/s], Decompressed: 2028
Downloaded: 2687 file(s) [attempted 2687/8546 = 31%, 1358 KB/s], Decompressed: 2028
Downloaded: 2731 file(s) [attempted 2731/8546 = 31%, 77 KB/s], Decompressed: 2028
Downloaded: 2769 file(s) [attempted 2769/8546 = 32%, 43 KB/s], Decompressed: 2028
Downloaded: 2809 file(s) [attempted 2809/8546 = 32%, 673 KB/s], Decompressed: 2028
Downloaded: 2846 file(s) [attempted 2846/8546 = 33%, 227 KB/s], Decompressed: 2028
Downloaded: 2887 file(s) [attempted 2887/8546 = 33%, 243 KB/s], Decompressed: 2028
Downloaded: 2931 file(s) [attempted 2931/8546 = 34%, 254 KB/s], Decompressed: 2028
Downloaded: 2965 file(s) [attempted 2965/8546 = 34%, 826 KB/s], Decompressed: 2028
Downloaded: 3012 file(s) [attempted 3012/8546 = 35%, 222 KB/s], Decompressed: 2028
Downloaded: 3049 file(s) [attempted 3049/8546 = 35%, 90 KB/s], Decompressed: 2028
Downloaded: 3087 file(s) [attempted 3087/8546 = 36%, 148 KB/s], Decompressed: 2028
Downloaded: 3131 file(s) [attempted 3131/8546 = 36%, 154 KB/s], Decompressed: 2028
Downloaded: 3171 file(s) [attempted 3171/8546 = 37%, 318 KB/s], Decompressed: 2028
Downloaded: 3212 file(s) [attempted 3212/8546 = 37%, 237 KB/s], Decompressed: 2549
Downloaded: 3252 file(s) [attempted 3252/8546 = 38%, 660 KB/s], Decompressed: 2549
Downloaded: 3296 file(s) [attempted 3296/8546 = 38%, 98 KB/s], Decompressed: 2549
Downloaded: 3333 file(s) [attempted 3333/8546 = 39%, 211 KB/s], Decompressed: 2549
Downloaded: 3371 file(s) [attempted 3371/8546 = 39%, 58 KB/s], Decompressed: 2549
Downloaded: 3415 file(s) [attempted 3415/8546 = 39%, 614 KB/s], Decompressed: 2549
Downloaded: 3462 file(s) [attempted 3462/8546 = 40%, 253 KB/s], Decompressed: 2549
Downloaded: 3509 file(s) [attempted 3509/8546 = 41%, 160 KB/s], Decompressed: 2549
Downloaded: 3553 file(s) [attempted 3553/8546 = 41%, 623 KB/s], Decompressed: 2549
Downloaded: 3594 file(s) [attempted 3594/8546 = 42%, 538 KB/s], Decompressed: 2549
Downloaded: 3618 file(s) [attempted 3618/8546 = 42%, 1128 KB/s], Decompressed: 2549
Downloaded: 3668 file(s) [attempted 3668/8546 = 42%, 135 KB/s], Decompressed: 2549
Downloaded: 3716 file(s) [attempted 3716/8546 = 43%, 332 KB/s], Decompressed: 2549
Downloaded: 3763 file(s) [attempted 3763/8546 = 44%, 25 KB/s], Decompressed: 2549
Downloaded: 3810 file(s) [attempted 3810/8546 = 44%, 335 KB/s], Decompressed: 2549
Downloaded: 3854 file(s) [attempted 3854/8546 = 45%, 480 KB/s], Decompressed: 2549
Downloaded: 3895 file(s) [attempted 3895/8546 = 45%, 820 KB/s], Decompressed: 2549
Downloaded: 3933 file(s) [attempted 3933/8546 = 46%, 252 KB/s], Decompressed: 2549
Downloaded: 3969 file(s) [attempted 3969/8546 = 46%, 313 KB/s], Decompressed: 2549
Downloaded: 4013 file(s) [attempted 4013/8546 = 46%, 883 KB/s], Decompressed: 2549
Downloaded: 4059 file(s) [attempted 4059/8546 = 47%, 790 KB/s], Decompressed: 3212
Downloaded: 4091 file(s) [attempted 4091/8546 = 47%, 650 KB/s], Decompressed: 3212
Downloaded: 4132 file(s) [attempted 4132/8546 = 48%, 1040 KB/s], Decompressed: 3212
Downloaded: 4176 file(s) [attempted 4176/8546 = 48%, 79 KB/s], Decompressed: 3212
Downloaded: 4216 file(s) [attempted 4216/8546 = 49%, 112 KB/s], Decompressed: 3212
Downloaded: 4257 file(s) [attempted 4257/8546 = 49%, 418 KB/s], Decompressed: 3212
Downloaded: 4294 file(s) [attempted 4294/8546 = 50%, 56 KB/s], Decompressed: 3212
Downloaded: 4335 file(s) [attempted 4335/8546 = 50%, 123 KB/s], Decompressed: 3212
Downloaded: 4379 file(s) [attempted 4379/8546 = 51%, 69 KB/s], Decompressed: 3212
Downloaded: 4423 file(s) [attempted 4423/8546 = 51%, 187 KB/s], Decompressed: 3212
Downloaded: 4460 file(s) [attempted 4460/8546 = 52%, 498 KB/s], Decompressed: 3212
Downloaded: 4504 file(s) [attempted 4504/8546 = 52%, 449 KB/s], Decompressed: 3212
Downloaded: 4538 file(s) [attempted 4538/8546 = 53%, 984 KB/s], Decompressed: 3212
Downloaded: 4582 file(s) [attempted 4582/8546 = 53%, 22 KB/s], Decompressed: 3212
Downloaded: 4626 file(s) [attempted 4626/8546 = 54%, 165 KB/s], Decompressed: 3212
Downloaded: 4666 file(s) [attempted 4666/8546 = 54%, 165 KB/s], Decompressed: 3212
Downloaded: 4710 file(s) [attempted 4710/8546 = 55%, 54 KB/s], Decompressed: 3212
Downloaded: 4744 file(s) [attempted 4744/8546 = 55%, 244 KB/s], Decompressed: 3212
Downloaded: 4781 file(s) [attempted 4781/8546 = 55%, 113 KB/s], Decompressed: 3212
Downloaded: 4829 file(s) [attempted 4829/8546 = 56%, 132 KB/s], Decompressed: 3212
Downloaded: 4869 file(s) [attempted 4869/8546 = 56%, 43 KB/s], Decompressed: 3212
Downloaded: 4917 file(s) [attempted 4917/8546 = 57%, 92 KB/s], Decompressed: 3212
Downloaded: 4961 file(s) [attempted 4961/8546 = 58%, 208 KB/s], Decompressed: 3212
Downloaded: 4994 file(s) [attempted 4994/8546 = 58%, 130 KB/s], Decompressed: 3212
Downloaded: 5028 file(s) [attempted 5028/8546 = 58%, 702 KB/s], Decompressed: 3212
Downloaded: 5072 file(s) [attempted 5072/8546 = 59%, 131 KB/s], Decompressed: 3212
Downloaded: 5113 file(s) [attempted 5113/8546 = 59%, 48 KB/s], Decompressed: 4037
Downloaded: 5160 file(s) [attempted 5160/8546 = 60%, 762 KB/s], Decompressed: 4037
Downloaded: 5204 file(s) [attempted 5204/8546 = 60%, 469 KB/s], Decompressed: 4037
Downloaded: 5245 file(s) [attempted 5245/8546 = 61%, 39 KB/s], Decompressed: 4037
Downloaded: 5279 file(s) [attempted 5279/8546 = 61%, 1720 KB/s], Decompressed: 4037
Downloaded: 5319 file(s) [attempted 5319/8546 = 62%, 23 KB/s], Decompressed: 4037
Downloaded: 5367 file(s) [attempted 5367/8546 = 62%, 314 KB/s], Decompressed: 4037
Downloaded: 5411 file(s) [attempted 5411/8546 = 63%, 703 KB/s], Decompressed: 4037
Downloaded: 5451 file(s) [attempted 5451/8546 = 63%, 22 KB/s], Decompressed: 4037
Downloaded: 5495 file(s) [attempted 5495/8546 = 64%, 155 KB/s], Decompressed: 4037
Downloaded: 5532 file(s) [attempted 5532/8546 = 64%, 276 KB/s], Decompressed: 4037
Downloaded: 5573 file(s) [attempted 5573/8546 = 65%, 692 KB/s], Decompressed: 4037
Downloaded: 5617 file(s) [attempted 5617/8546 = 65%, 999 KB/s], Decompressed: 4037
Downloaded: 5657 file(s) [attempted 5657/8546 = 66%, 696 KB/s], Decompressed: 4037
Downloaded: 5695 file(s) [attempted 5695/8546 = 66%, 552 KB/s], Decompressed: 4037
Downloaded: 5735 file(s) [attempted 5735/8546 = 67%, 49 KB/s], Decompressed: 4037
Downloaded: 5772 file(s) [attempted 5772/8546 = 67%, 487 KB/s], Decompressed: 4037
Downloaded: 5816 file(s) [attempted 5816/8546 = 68%, 263 KB/s], Decompressed: 4037
Downloaded: 5854 file(s) [attempted 5854/8546 = 68%, 186 KB/s], Decompressed: 4037
Downloaded: 5894 file(s) [attempted 5894/8546 = 68%, 188 KB/s], Decompressed: 4037
Downloaded: 5938 file(s) [attempted 5938/8546 = 69%, 643 KB/s], Decompressed: 4037
Downloaded: 5975 file(s) [attempted 5975/8546 = 69%, 136 KB/s], Decompressed: 4037
Downloaded: 6016 file(s) [attempted 6016/8546 = 70%, 89 KB/s], Decompressed: 4037
Downloaded: 6057 file(s) [attempted 6057/8546 = 70%, 257 KB/s], Decompressed: 4037
Downloaded: 6094 file(s) [attempted 6094/8546 = 71%, 142 KB/s], Decompressed: 4037
Downloaded: 6134 file(s) [attempted 6134/8546 = 71%, 244 KB/s], Decompressed: 4037
Downloaded: 6175 file(s) [attempted 6175/8546 = 72%, 1204 KB/s], Decompressed: 4037
Downloaded: 6216 file(s) [attempted 6216/8546 = 72%, 368 KB/s], Decompressed: 4037
Downloaded: 6256 file(s) [attempted 6256/8546 = 73%, 213 KB/s], Decompressed: 4037
Downloaded: 6297 file(s) [attempted 6297/8546 = 73%, 280 KB/s], Decompressed: 4037
Downloaded: 6334 file(s) [attempted 6334/8546 = 74%, 88 KB/s], Decompressed: 5106
Downloaded: 6371 file(s) [attempted 6371/8546 = 74%, 361 KB/s], Decompressed: 5106
Downloaded: 6415 file(s) [attempted 6415/8546 = 75%, 405 KB/s], Decompressed: 5106
Downloaded: 6459 file(s) [attempted 6459/8546 = 75%, 69 KB/s], Decompressed: 5106
Downloaded: 6496 file(s) [attempted 6496/8546 = 76%, 282 KB/s], Decompressed: 5106
Downloaded: 6534 file(s) [attempted 6534/8546 = 76%, 137 KB/s], Decompressed: 5106
Downloaded: 6574 file(s) [attempted 6574/8546 = 76%, 84 KB/s], Decompressed: 5106
Downloaded: 6618 file(s) [attempted 6618/8546 = 77%, 336 KB/s], Decompressed: 5106
Downloaded: 6662 file(s) [attempted 6662/8546 = 77%, 394 KB/s], Decompressed: 5106
Downloaded: 6702 file(s) [attempted 6702/8546 = 78%, 62 KB/s], Decompressed: 5106
Downloaded: 6740 file(s) [attempted 6740/8546 = 78%, 256 KB/s], Decompressed: 5106
Downloaded: 6781 file(s) [attempted 6781/8546 = 79%, 76 KB/s], Decompressed: 5106
Downloaded: 6821 file(s) [attempted 6821/8546 = 79%, 1242 KB/s], Decompressed: 5106
Downloaded: 6862 file(s) [attempted 6862/8546 = 80%, 263 KB/s], Decompressed: 5106
Downloaded: 6902 file(s) [attempted 6902/8546 = 80%, 557 KB/s], Decompressed: 5106
Downloaded: 6943 file(s) [attempted 6943/8546 = 81%, 25 KB/s], Decompressed: 5106
Downloaded: 6990 file(s) [attempted 6990/8546 = 81%, 884 KB/s], Decompressed: 5106
Downloaded: 7034 file(s) [attempted 7034/8546 = 82%, 157 KB/s], Decompressed: 5106
Downloaded: 7075 file(s) [attempted 7075/8546 = 82%, 371 KB/s], Decompressed: 5106
Downloaded: 7119 file(s) [attempted 7119/8546 = 83%, 397 KB/s], Decompressed: 5106
Downloaded: 7156 file(s) [attempted 7156/8546 = 83%, 43 KB/s], Decompressed: 5106
Downloaded: 7200 file(s) [attempted 7200/8546 = 84%, 237 KB/s], Decompressed: 5106
Downloaded: 7237 file(s) [attempted 7237/8546 = 84%, 77 KB/s], Decompressed: 5106
Downloaded: 7281 file(s) [attempted 7281/8546 = 85%, 268 KB/s], Decompressed: 5106
Downloaded: 7322 file(s) [attempted 7322/8546 = 85%, 454 KB/s], Decompressed: 5106
Downloaded: 7359 file(s) [attempted 7359/8546 = 86%, 99 KB/s], Decompressed: 5106
Downloaded: 7403 file(s) [attempted 7403/8546 = 86%, 73 KB/s], Decompressed: 5106
Downloaded: 7450 file(s) [attempted 7450/8546 = 87%, 288 KB/s], Decompressed: 5106
Downloaded: 7494 file(s) [attempted 7494/8546 = 87%, 667 KB/s], Decompressed: 5106
Downloaded: 7532 file(s) [attempted 7532/8546 = 88%, 950 KB/s], Decompressed: 5106
Downloaded: 7579 file(s) [attempted 7579/8546 = 88%, 26 KB/s], Decompressed: 5106
Downloaded: 7619 file(s) [attempted 7619/8546 = 89%, 225 KB/s], Decompressed: 5106
Downloaded: 7657 file(s) [attempted 7657/8546 = 89%, 255 KB/s], Decompressed: 5106
Downloaded: 7701 file(s) [attempted 7701/8546 = 90%, 162 KB/s], Decompressed: 5106
Downloaded: 7741 file(s) [attempted 7741/8546 = 90%, 124 KB/s], Decompressed: 5106
Downloaded: 7782 file(s) [attempted 7782/8546 = 91%, 883 KB/s], Decompressed: 5106
Downloaded: 7819 file(s) [attempted 7819/8546 = 91%, 123 KB/s], Decompressed: 5106
Downloaded: 7856 file(s) [attempted 7856/8546 = 91%, 473 KB/s], Decompressed: 5106
Downloaded: 7904 file(s) [attempted 7904/8546 = 92%, 21 KB/s], Decompressed: 6327
Downloaded: 7951 file(s) [attempted 7951/8546 = 93%, 514 KB/s], Decompressed: 6327
Downloaded: 7992 file(s) [attempted 7992/8546 = 93%, 3862 KB/s], Decompressed: 6327
Downloaded: 8032 file(s) [attempted 8032/8546 = 93%, 1753 KB/s], Decompressed: 6327
Downloaded: 8073 file(s) [attempted 8073/8546 = 94%, 238 KB/s], Decompressed: 6327
Downloaded: 8110 file(s) [attempted 8110/8546 = 94%, 582 KB/s], Decompressed: 6327
Downloaded: 8154 file(s) [attempted 8154/8546 = 95%, 78 KB/s], Decompressed: 6327
Downloaded: 8201 file(s) [attempted 8201/8546 = 95%, 117 KB/s], Decompressed: 6327
Downloaded: 8249 file(s) [attempted 8249/8546 = 96%, 24 KB/s], Decompressed: 6327
Downloaded: 8286 file(s) [attempted 8286/8546 = 96%, 25 KB/s], Decompressed: 6327
Downloaded: 8323 file(s) [attempted 8323/8546 = 97%, 513 KB/s], Decompressed: 6327
Downloaded: 8367 file(s) [attempted 8367/8546 = 97%, 144 KB/s], Decompressed: 6327
Downloaded: 8408 file(s) [attempted 8408/8546 = 98%, 69 KB/s], Decompressed: 6327
Downloaded: 8448 file(s) [attempted 8448/8546 = 98%, 234 KB/s], Decompressed: 6327
Downloaded: 8485 file(s) [attempted 8485/8546 = 99%, 271 KB/s], Decompressed: 6327
Downloaded: 8529 file(s) [attempted 8529/8546 = 99%, 109 KB/s], Decompressed: 6327
Downloaded: 8546 file(s) [attempted 8546/8546 = 100%, 109 KB/s], Decompressed: 6327

lake build

✔ [2071/2074] Built PrimeNumberTheoremAnd.Auxiliary (41s)
✔ [3001/3008] Built PrimeNumberTheoremAnd.Sobolev (29s)
✔ [3021/3026] Built PrimeNumberTheoremAnd.Fourier (3.6s)
✔ [3022/3027] Built Architect.Basic (5.7s)
✔ [3023/3027] Built Architect.Command (917ms)
✔ [3024/3027] Built Architect.CollectUsed (945ms)
✔ [3025/3027] Built Architect.Content (959ms)
✔ [3026/3031] Built Architect.Attribute (1.6s)
✔ [3027/3032] Built Architect.Tactic (1.5s)
✔ [3028/3032] Built Architect.Output (1.8s)
✔ [3030/3033] Built Architect.Load (1.0s)
✔ [3031/3037] Built Architect (805ms)
✔ [3059/3068] Built PrimeNumberTheoremAnd.Defs (25s)
✔ [3544/3554] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic (3.6s)
✔ [3546/3554] Built PrimeNumberTheoremAnd.Rectangle (3.0s)
✔ [3550/3555] Built PrimeNumberTheoremAnd.Tactic.AdditiveCombination (2.3s)
✔ [3552/3560] Built PrimeNumberTheoremAnd.ZetaConj (5.2s)
✔ [3554/3561] Built PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions (10s)
✔ [3557/3562] Built PrimeNumberTheoremAnd.EulerMaclaurin (5.5s)
✔ [3561/3567] Built PrimeNumberTheoremAnd.ResidueCalcOnRectangles (8.0s)
✔ [3563/3567] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (2.7s)
✔ [3565/3569] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Norm (1.5s)
✔ [3566/3569] Built PrimeNumberTheoremAnd.ZetaBounds (48s)
✔ [3570/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorSupport (8.8s)
✔ [3573/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit (2.7s)
✔ [3575/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor (3.5s)
✔ [3576/3588] Built PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Annulus (1.9s)
✔ [3577/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalProduct (2.4s)
✔ [3578/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorIndex (2.1s)
✔ [3579/3588] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorUnits (1.9s)
✔ [3580/3590] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorConvergence (3.1s)
✔ [3581/3590] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorFiber (2.7s)
✔ [3583/3592] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement (4.2s)
✔ [3585/3592] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorPartialProductFactor (2.7s)
✔ [3587/3596] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientConvergence (3.8s)
✔ [3589/3598] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientRemovable (2.8s)
✔ [3592/3598] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor (2.4s)
✔ [3595/3601] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization (2.9s)
✔ [3610/3629] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Exp (1.9s)
✔ [3611/3629] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorHolomorphic (1.8s)
✔ [3613/3631] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic (2.6s)
✔ [3615/3631] Built PrimeNumberTheoremAnd.MellinCalculus (63s)
✔ [3616/3631] Built PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support (2.5s)
✔ [3618/3632] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.PosLog (3.9s)
✔ [3620/3632] Built PrimeNumberTheoremAnd.SmoothExistence (21s)
✔ [3622/3633] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth (2.1s)
ℹ [3626/3636] Built PrimeNumberTheoremAnd.MediumPNT (63s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3632/3638] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (13s)
✔ [3634/3639] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Growth (4.2s)
✔ [3636/3646] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability (4.4s)
✔ [3638/3648] Built PrimeNumberTheoremAnd.Backlund.ZeroCountCrude (186s)
✔ [3640/3651] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics (23s)
✔ [3644/3655] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults (16s)
✔ [3647/3655] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic (3.0s)
✔ [3650/3656] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg (4.7s)
⚠ [3651/3656] Built PrimeNumberTheoremAnd.StrongPNT (74s)
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`
✔ [3653/3656] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds (32s)
✔ [3654/3656] Built PrimeNumberTheoremAnd.BorelCaratheodory (65s)
✔ [3655/3660] Built PrimeNumberTheoremAnd.BrunTitchmarsh (5.4s)
✔ [3778/3784] Built LeanCert.Core.Interval (3.1s)
⚠ [3779/3784] Built PrimeNumberTheoremAnd.Wiener (45s)
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`
✔ [3780/3784] Built LeanCert.Core.IntervalRat.Basic (32s)
⚠ [3781/3784] Built PrimeNumberTheoremAnd.Consequences (45s)
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`
✔ [3782/3784] Built LeanCert.Tactic.IntervalAuto.Types (4.7s)
✔ [3783/3794] Built LeanCert.Tactic.IntervalAuto.Norm (3.3s)
✔ [3788/3794] Built LeanCert.Core.Expr (3.7s)
✔ [3789/3795] Built LeanCert.Meta.Numeral (3.0s)
✔ [3790/3795] Built LeanCert.Meta.ToExpr (3.8s)
✔ [3791/3795] Built LeanCert.Tactic.IntervalAuto.Extract (2.5s)
✔ [3792/3795] Built LeanCert.Core.Support (2.2s)
✔ [3793/3796] Built LeanCert.Tactic.IntervalAuto.Parse (4.1s)
✔ [3794/3796] Built LeanCert.Tactic.IntervalAuto.Diagnostic (2.5s)
✔ [3795/3797] Built LeanCert.Core.IntervalRat.Transcendental (3.2s)
✔ [3796/3799] Built LeanCert.Core.IntervalRat.LogReduction (3.4s)
✔ [3809/3819] Built LeanCert.Core.DerivativeIntervals (2.2s)
✔ [3812/3822] Built LeanCert.Core.TrigReduction (2.6s)
✔ [3813/3822] Built LeanCert.Core.Taylor (4.5s)
✔ [3814/3823] Built LeanCert.Core.IntervalRat.Taylor (9.3s)
✔ [3815/3824] Built LeanCert.Core.IntervalRat.TrigReduced (2.3s)
✔ [3816/3825] Built LeanCert.Core.IntervalReal (2.0s)
✔ [3817/3826] Built LeanCert.Core.IntervalRealEndpoints (2.9s)
✔ [3818/3826] Built LeanCert.Engine.Eval.Core (4.5s)
✔ [3819/3828] Built LeanCert.Engine.Eval.Extended (2.9s)
✔ [3820/3833] Built LeanCert.Tactic.Bound.Lemmas (2.1s)
✔ [3821/3833] Built LeanCert.Contrib.Sinc (3.0s)
✔ [3822/3833] Built LeanCert.Engine.IntervalEval (1.0s)
✔ [3823/3833] Built LeanCert.Engine.AD.Basic (2.1s)
✔ [3824/3833] Built LeanCert.Engine.AD.Transcendental (3.1s)
✔ [3825/3833] Built LeanCert.Engine.AD.Eval (2.1s)
✔ [3826/3833] Built LeanCert.Engine.AD.Correctness (2.7s)
✔ [3827/3834] Built LeanCert.Engine.AD.Computable (2.6s)
✔ [3828/3834] Built LeanCert.Engine.AD.PartialCorrectness (4.5s)
✔ [3829/3834] Built LeanCert.Engine.TaylorModel.Core (5.0s)
✔ [3830/3834] Built LeanCert.Engine.AD (1.0s)
✔ [3831/3836] Built LeanCert.Meta.ProveSupported (3.9s)
✔ [3832/3837] Built LeanCert.Tactic.IntervalAuto.ProveCommon (4.0s)
✔ [3834/3837] Built LeanCert.Tactic.IntervalAuto.Basic (2.4s)
✔ [3835/3837] Built LeanCert.Engine.TaylorModel.ExpLog (4.7s)
✔ [3836/3841] Built LeanCert.Engine.TaylorModel.Trig (6.1s)
✔ [3842/3849] Built LeanCert.Engine.TaylorModel.Special (2.1s)
✔ [3846/3853] Built LeanCert.Engine.Integrate (3.8s)
✔ [3847/3853] Built LeanCert.Engine.TaylorModel.Hyperbolic (7.1s)
✔ [3848/3856] Built LeanCert.Engine.TaylorModel.Integral (2.7s)
✔ [3849/3856] Built LeanCert.Engine.TaylorModel.Functions (1.0s)
✔ [3850/3856] Built LeanCert.Core.Dyadic (2.0s)
✔ [3851/3856] Built LeanCert.Engine.TaylorModel.Expr (3.4s)
✔ [3852/3856] Built LeanCert.Core.IntervalDyadic (4.8s)
✔ [3853/3860] Built LeanCert.Engine.TaylorModel (1.9s)
✔ [3854/3860] Built LeanCert.Engine.IntervalEvalDyadic (2.0s)
✔ [3855/3861] Built LeanCert.Engine.IntervalEvalRefined (2.7s)
✔ [3856/3861] Built LeanCert.Engine.Affine.Basic (3.9s)
✔ [3857/3861] Built LeanCert.Engine.Optimization.Box (2.2s)
✔ [3858/3864] Built LeanCert.Engine.Affine.Nonlinear (3.3s)
✔ [3859/3864] Built LeanCert.Engine.Affine.Transcendental (2.9s)
✔ [3860/3864] Built LeanCert.Engine.Optimize (4.0s)
✔ [3861/3865] Built LeanCert.Engine.IntervalEvalAffine (3.0s)
✔ [3862/3866] Built LeanCert.Engine.Optimization.Gradient (3.4s)
✔ [3863/3866] Built LeanCert.Engine.RootFinding.Basic (3.3s)
✔ [3864/3867] Built LeanCert.Engine.Optimization.Global (10s)
✔ [3865/3868] Built LeanCert.Engine.RootFinding.Bisection (3.3s)
✔ [3866/3870] Built LeanCert.Engine.RootFinding.Newton (3.2s)
✔ [3867/3871] Built LeanCert.Engine.RootFinding.MVTBounds (4.1s)
✔ [3868/3871] Built LeanCert.Engine.RootFinding.Contraction (3.6s)
✔ [3869/3871] Built LeanCert.Meta.ProveContinuous (3.4s)
✔ [3870/3873] Built LeanCert.Engine.RootFinding.Main (1.0s)
✔ [3871/3874] Built LeanCert.Validity.Bounds.Core (2.1s)
✔ [3872/3876] Built LeanCert.Validity.Bounds.WithInv (2.2s)
✔ [3873/3878] Built LeanCert.Validity.Bounds.Smart (2.3s)
✔ [3874/3879] Built LeanCert.Validity.Bounds.Bridge (2.3s)
✔ [3875/3879] Built LeanCert.Validity.Integration (3.5s)
✔ [3876/3881] Built LeanCert.Validity.Bounds.Basic (2.0s)
✔ [3877/3881] Built LeanCert.Validity.DyadicBounds (2.2s)
✔ [3878/3882] Built LeanCert.Validity.Bounds (4.5s)
✔ [3879/3883] Built LeanCert.Engine.Optimization.BoundVerify (2.4s)
✔ [3880/3883] Built LeanCert.Tactic.IntervalAuto.Multivariate (4.1s)
✔ [3881/3884] Built LeanCert.Tactic.IntervalAuto.Bound (20s)
✔ [3882/3885] Built LeanCert.Tactic.IntervalAuto.OptBound (2.8s)
✔ [3883/3886] Built LeanCert.Tactic.IntervalAuto.RootBound (2.8s)
✔ [3884/3889] Built LeanCert.Tactic.IntervalAuto.PointIneq (11s)
✔ [3885/3889] Built LeanCert.Tactic.IntervalAuto.Subdiv (5.9s)
✔ [3886/3899] Built LeanCert.Tactic.IntervalAuto.Adaptive (5.0s)
✔ [3888/3899] Built PrimeNumberTheoremAnd.GeneralMeromorphic (2.7s)
✔ [3889/3899] Built PrimeNumberTheoremAnd.HadamardFactorization (1.2s)
✔ [3890/3899] Built PrimeNumberTheoremAnd.HoffsteinLockhart (5.2s)
✔ [3891/3899] Built PrimeNumberTheoremAnd.IEANTN.KLN (9.3s)
⚠ [3892/3899] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta (4.0s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3893/3900] Built LeanCert.Tactic.IntervalAuto (2.9s)
✔ [3895/3900] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv (6.1s)
✔ [3896/3900] Built PrimeNumberTheoremAnd.IEANTN.LogTables (28s)
✖ [3898/3901] Building PrimeNumberTheoremAnd.IEANTN.Mertens (20s)
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/Mertens.lean -o /apx/source/.lake/build/lib/lean/PrimeNumberTheoremAnd/IEANTN/Mertens.olean -i /apx/source/.lake/build/lib/lean/PrimeNumberTheoremAnd/IEANTN/Mertens.ilean -c /apx/source/.lake/build/ir/PrimeNumberTheoremAnd/IEANTN/Mertens.c --setup /apx/source/.lake/build/ir/PrimeNumberTheoremAnd/IEANTN/Mertens.setup.json --json
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:1152: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`
error: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1246:4: Type mismatch: After simplification, term
  Summable.neg this
 has type
  @Summable ℝ Nat.Primes Real.instAddCommGroup.toAddCommMonoid PseudoMetricSpace.toUniformSpace.toTopologicalSpace
    (fun b ↦ -log (1 + -z b)) (SummationFilter.unconditional Nat.Primes)
but is expected to have type
  @Summable ℝ Nat.Primes Real.instAddCommMonoid PseudoMetricSpace.toUniformSpace.toTopologicalSpace
    (fun p ↦ -log (1 - z p)) (SummationFilter.unconditional Nat.Primes)
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1305:16: declaration uses `sorry`
error: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1332:2: `grind` failed
case grind.2
s : ℝ
hs : 1 < s
h :
  ¬(s - 1) *
        ∫ (a : ℝ) in Set.Ioi 1,
          (∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                1 -
              log (log 2)) *
            a ^ (-s) ∂MeasureTheory.volume =
      ∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume + 1 -
        log (log 2)
h_1 : ¬-s + 1 = 0
⊢ False
[grind] Goal diagnostics
  [facts] Asserted facts
    [prop] 1 < s
    [prop] ¬(s - 1) *
              ∫ (a : ℝ) in Set.Ioi 1,
                (∫ (t : ℝ) in Set.Ioi 2,
                        (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                      1 -
                    log (log 2)) *
                  a ^ (-s) ∂MeasureTheory.volume =
            ∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                1 -
              log (log 2)
    [prop] ∫ (a : ℝ) in Set.Ioi 1,
            (∫ (t : ℝ) in Set.Ioi 2,
                    (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                  1 -
                log (log 2)) *
              a ^ (-s) ∂MeasureTheory.volume =
          (∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                1 -
              log (log 2)) *
            ∫ (x : ℝ) in Set.Ioi 1, x ^ (-s) ∂MeasureTheory.volume
    [prop] -s < -1 → 0 < 1 → ∫ (x : ℝ) in Set.Ioi 1, x ^ (-s) ∂MeasureTheory.volume = -1 ^ (-s + 1) * (-s + 1)⁻¹
    [prop] if -s + 1 = 0 then (-s + 1)⁻¹ = 0 else (-s + 1) * (-s + 1)⁻¹ = 1
    [prop] 1 ^ (-s + 1) = 1
    [prop] ¬-s + 1 = 0
  [eqc] True propositions
    [prop] (-s + 1) * (-s + 1)⁻¹ = 1
    [prop] 1 < s
    [prop] if -s + 1 = 0 then (-s + 1)⁻¹ = 0 else (-s + 1) * (-s + 1)⁻¹ = 1
    [prop] ∫ (x : ℝ) in Set.Ioi 1, x ^ (-s) ∂MeasureTheory.volume = -1 ^ (-s + 1) * (-s + 1)⁻¹
    [prop] -s < -1
    [prop] 0 < 1
    [prop] -s < -1 → 0 < 1 → ∫ (x : ℝ) in Set.Ioi 1, x ^ (-s) ∂MeasureTheory.volume = -1 ^ (-s + 1) * (-s + 1)⁻¹
    [prop] 0 < 1 → ∫ (x : ℝ) in Set.Ioi 1, x ^ (-s) ∂MeasureTheory.volume = -1 ^ (-s + 1) * (-s + 1)⁻¹
  [eqc] False propositions
    [prop] -s + 1 = 0
    [prop] (s - 1) *
            ∫ (a : ℝ) in Set.Ioi 1,
              (∫ (t : ℝ) in Set.Ioi 2,
                      (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                    1 -
                  log (log 2)) *
                a ^ (-s) ∂MeasureTheory.volume =
          ∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
              1 -
            log (log 2)
  [eqc] Equivalence classes
    [eqc] {1,
        (-s + 1) * (-s + 1)⁻¹,
        ((s - 1) *
              ∫ (a : ℝ) in Set.Ioi 1,
                (∫ (t : ℝ) in Set.Ioi 2,
                        (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                      1 -
                    log (log 2)) *
                  a ^ (-s) ∂MeasureTheory.volume -
            (∫ (t : ℝ) in Set.Ioi 2,
                  (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                1 -
              log (log 2))) *
          ((s - 1) *
                ∫ (a : ℝ) in Set.Ioi 1,
                  (∫ (t : ℝ) in Set.Ioi 2,
                          (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                        1 -
                      log (log 2)) *
                    a ^ (-s) ∂MeasureTheory.volume -
              (∫ (t : ℝ) in Set.Ioi 2,
                    (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                  1 -
                log (log 2)))⁻¹,
        1 ^ (-s + 1)}
    [eqc] {(∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
              1 -
            log (log 2)) *
          ∫ (x : ℝ) in Set.Ioi 1, x ^ (-s) ∂MeasureTheory.volume,
        ∫ (a : ℝ) in Set.Ioi 1,
          (∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                1 -
              log (log 2)) *
            a ^ (-s) ∂MeasureTheory.volume}
    [eqc] {-1, -1 ^ (-s + 1)}
    [eqc] {-1 ^ (-s + 1) * (-s + 1)⁻¹, ∫ (x : ℝ) in Set.Ioi 1, x ^ (-s) ∂MeasureTheory.volume}
  [cases] Case analyses
    [cases] [2/2]: if -s + 1 = 0 then (-s + 1)⁻¹ = 0 else (-s + 1) * (-s + 1)⁻¹ = 1
      [cases] source: E-matching `@integral_Ioi_rpow_of_lt (-s)`
  [ematch] E-matching patterns
    [thm] MeasureTheory.integral_const_mul γ
              (· ^
                (-s)): [@MeasureTheory.integral `[ℝ] `[ℝ] `[NonUnitalNormedRing.toNormedAddCommGroup] `[NormedAlgebra.toNormedSpace
           ℝ] #1 #0 `[fun a ↦
           (∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                 1 -
               log (log 2)) *
             a ^ (-s)]]
    [thm] @integral_Ioi_rpow_of_lt
              (-s): [@MeasureTheory.integral `[ℝ] `[ℝ] `[normedAddCommGroup] `[RCLike.toInnerProductSpaceReal.toNormedSpace] `[measurableSpace] (@MeasureTheory.Measure.restrict `[ℝ] `[measurableSpace] `[MeasureTheory.volume] (@Set.Ioi `[ℝ] `[instPreorder] #1)) `[fun
             x ↦
           x ^ (-s)]]
    [thm] one_rpow: [@HPow.hPow `[ℝ] `[ℝ] `[ℝ] `[instHPow] `[1] #0]
    [thm] Nat.pow_pos: [@HPow.hPow `[ℕ] `[ℕ] `[ℕ] `[instHPow] #2 #1]
    [thm] Nat.div_pow_of_pos: [@HPow.hPow `[ℕ] `[ℕ] `[ℕ] `[instHPow] #2 #1]
  [linarith] Linarith assignment for `ℝ`
    [assign] s := 2
    [assign] log (log 2) := 0
    [assign] log 2 := 9
    [assign] ∫ (a : ℝ) in Set.Ioi 1,
          (∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                1 -
              log (log 2)) *
            a ^ (-s) ∂MeasureTheory.volume := 0
    [assign] ∫ (t : ℝ) in Set.Ioi 2,
          (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume := 0
    [assign] ∫ (a : ℝ) in Set.Ioi 1,
          (∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                1 -
              log (log 2)) *
            a ^ (-s) ∂MeasureTheory.volume := 0
    [assign] ∫ (x : ℝ) in Set.Ioi 1, x ^ (-s) ∂MeasureTheory.volume := 20
    [assign] 「1 ^ (-s + 1)」 := 1
    [assign] ∫ (x : ℝ) in Set.Ioi 1, x ^ (-s) ∂MeasureTheory.volume := 0
  [ring] Ring `ℝ`
    [basis] Basis
      [_] (s *
                          ∫ (a : ℝ) in Set.Ioi 1,
                            (∫ (t : ℝ) in Set.Ioi 2,
                                    (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                  1 -
                                log (log 2)) *
                              a ^ (-s) ∂MeasureTheory.volume) *
                        ((s - 1) *
                              ∫ (a : ℝ) in Set.Ioi 1,
                                (∫ (t : ℝ) in Set.Ioi 2,
                                        (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) *
                                          (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                      1 -
                                    log (log 2)) *
                                  a ^ (-s) ∂MeasureTheory.volume -
                            (∫ (t : ℝ) in Set.Ioi 2,
                                  (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                1 -
                              log (log 2)))⁻¹ +
                      -1 *
                        ((∫ (a : ℝ) in Set.Ioi 1,
                            (∫ (t : ℝ) in Set.Ioi 2,
                                    (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                  1 -
                                log (log 2)) *
                              a ^ (-s) ∂MeasureTheory.volume) *
                          ((s - 1) *
                                ∫ (a : ℝ) in Set.Ioi 1,
                                  (∫ (t : ℝ) in Set.Ioi 2,
                                          (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) *
                                            (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                        1 -
                                      log (log 2)) *
                                    a ^ (-s) ∂MeasureTheory.volume -
                              (∫ (t : ℝ) in Set.Ioi 2,
                                    (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                  1 -
                                log (log 2)))⁻¹) +
                    -1 *
                      ((∫ (t : ℝ) in Set.Ioi 2,
                          (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume) *
                        ((s - 1) *
                              ∫ (a : ℝ) in Set.Ioi 1,
                                (∫ (t : ℝ) in Set.Ioi 2,
                                        (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) *
                                          (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                      1 -
                                    log (log 2)) *
                                  a ^ (-s) ∂MeasureTheory.volume -
                            (∫ (t : ℝ) in Set.Ioi 2,
                                  (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                1 -
                              log (log 2)))⁻¹) +
                  log (log 2) *
                    ((s - 1) *
                          ∫ (a : ℝ) in Set.Ioi 1,
                            (∫ (t : ℝ) in Set.Ioi 2,
                                    (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                  1 -
                                log (log 2)) *
                              a ^ (-s) ∂MeasureTheory.volume -
                        (∫ (t : ℝ) in Set.Ioi 2,
                              (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                            1 -
                          log (log 2)))⁻¹ +
                -1 *
                  ((s - 1) *
                        ∫ (a : ℝ) in Set.Ioi 1,
                          (∫ (t : ℝ) in Set.Ioi 2,
                                  (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                1 -
                              log (log 2)) *
                            a ^ (-s) ∂MeasureTheory.volume -
                      (∫ (t : ℝ) in Set.Ioi 2,
                            (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                          1 -
                        log (log 2)))⁻¹ +
              -1 =
            0
      [_] (∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume) *
                        ((s - 1) *
                              ∫ (a : ℝ) in Set.Ioi 1,
                                (∫ (t : ℝ) in Set.Ioi 2,
                                        (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) *
                                          (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                      1 -
                                    log (log 2)) *
                                  a ^ (-s) ∂MeasureTheory.volume -
                            (∫ (t : ℝ) in Set.Ioi 2,
                                  (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                1 -
                              log (log 2)))⁻¹ *
                      (-s + 1)⁻¹ +
                    -1 *
                      (log (log 2) *
                          ((s - 1) *
                                ∫ (a : ℝ) in Set.Ioi 1,
                                  (∫ (t : ℝ) in Set.Ioi 2,
                                          (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) *
                                            (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                        1 -
                                      log (log 2)) *
                                    a ^ (-s) ∂MeasureTheory.volume -
                              (∫ (t : ℝ) in Set.Ioi 2,
                                    (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                  1 -
                                log (log 2)))⁻¹ *
                        (-s + 1)⁻¹) +
                  (∫ (a : ℝ) in Set.Ioi 1,
                      (∫ (t : ℝ) in Set.Ioi 2,
                              (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                            1 -
                          log (log 2)) *
                        a ^ (-s) ∂MeasureTheory.volume) *
                    ((s - 1) *
                          ∫ (a : ℝ) in Set.Ioi 1,
                            (∫ (t : ℝ) in Set.Ioi 2,
                                    (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                  1 -
                                log (log 2)) *
                              a ^ (-s) ∂MeasureTheory.volume -
                        (∫ (t : ℝ) in Set.Ioi 2,
                              (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                            1 -
                          log (log 2)))⁻¹ +
                ((s - 1) *
                        ∫ (a : ℝ) in Set.Ioi 1,
                          (∫ (t : ℝ) in Set.Ioi 2,
                                  (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                1 -
                              log (log 2)) *
                            a ^ (-s) ∂MeasureTheory.volume -
                      (∫ (t : ℝ) in Set.Ioi 2,
                            (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                          1 -
                        log (log 2)))⁻¹ *
                  (-s + 1)⁻¹ +
              (-s + 1)⁻¹ =
            0
      [_] s * (-s + 1)⁻¹ + -1 * (-s + 1)⁻¹ + 1 = 0
      [_] 1 ^ (-s + 1) + -1 = 0
[grind] Diagnostics
  [thm] E-Matching instances
    [thm] extra_0 ↦ 1
    [thm] extra_1 ↦ 1
    [thm] one_rpow ↦ 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1799: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:1950: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:1987: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:2249: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:2267: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`
error: Lean exited with code 1
✔ [3899/3906] Built PrimeNumberTheoremAnd.EulerMascheroniBounds (9.4s)
✔ [3957/3972] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables (2.8s)
✔ [3960/3972] Built LeanCert.Engine.TaylorModel.Log1p (4.2s)
✔ [3962/3972] Built PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries (5.8s)
✔ [3965/3974] Built LeanCert.Examples.Li2Base (2.8s)
✔ [3966/3974] Built PrimeNumberTheoremAnd.IEANTN.PVIdentity (17s)
⚠ [3968/3975] Built LeanCert.Examples.Li2Bounds (2.3s)
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [3970/3976] Built PrimeNumberTheoremAnd.IEANTN.LiSeries (10s)
✔ [3971/3977] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (3.3s)
✔ [4108/4114] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables (46s)
✔ [4109/4117] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables (24s)
✔ [4112/4117] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (94s)
✔ [4114/4118] Built LeanCert.Engine.FinSumDyadic (4.9s)
✔ [4115/4118] Built LeanCert.Examples.BKLNW_a2_base (4.9s)
✔ [4116/4122] Built LeanCert.Engine.WitnessSum (2.5s)
✔ [4117/4146] Built LeanCert.Engine.ReflectiveSum (4.0s)
✔ [4118/4147] Built LeanCert.Tactic.VecUtil (2.1s)
✔ [4119/4147] Built LeanCert.Tactic.FinSumExpand (1.4s)
✔ [4121/4149] Built LeanCert.Examples.BKLNW_a2_reflective (91s)
✔ [4122/4149] Built LeanCert.Examples.BKLNW_a2_bounds (2.9s)
✔ [4123/4160] Built LeanCert.Examples.BKLNW_a2_pow2 (2.7s)
✔ [4154/4160] Built LeanCert.Engine.Chebyshev.Psi (2.9s)
✔ [4155/4162] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (6.1s)
✔ [4156/4164] Built LeanCert.Engine.ChebyshevPsi (1.0s)
⚠ [4158/4167] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP (22s)
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
⚠ [4163/4169] Built PrimeNumberTheoremAnd.IEANTN.Erdos392 (55s)
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`
✔ [4164/4169] Built LeanCert.Engine.Chebyshev.Theta (9.9s)
✔ [4166/4169] Built LeanCert.Engine.ChebyshevTheta (2.1s)
ℹ [4167/4174] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations (21s)
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.
✔ [4169/4175] Built LeanCert.Cert.Interval (1.3s)
✔ [4170/4176] Built LeanCert.ANT.Step (5.9s)
✔ [4171/4177] Built LeanCert.ANT.Abel (2.7s)
✔ [4172/4177] Built LeanCert.ANT.Asymp.Env (2.0s)
✔ [4173/4196] Built LeanCert.ANT.Asymp.Hyperbola (2.7s)
✔ [4174/4196] Built LeanCert.ANT.Asymp.Stieltjes (2.7s)
✔ [4175/4196] Built LeanCert.ANT.Asymp.Pointwise (2.7s)
✔ [4176/4196] Built LeanCert.Engine.Table (535ms)
✔ [4177/4201] Built LeanCert.ANT.Asymp.Checkers (2.7s)
✔ [4178/4201] Built LeanCert.ANT.Asymp.Inequality (2.5s)
✔ [4179/4201] Built LeanCert.Validity.AffineBounds (2.9s)
✔ [4180/4201] Built PrimeNumberTheoremAnd.Tactic.Simprocs (1.6s)
✔ [4182/4201] Built LeanCert.ANT.Asymp (2.3s)
✔ [4199/4203] Built LeanCert.Validity.AffineCover (2.2s)
✔ [4201/4204] Built PrimeCert.Interval (2.2s)
✔ [4202/4204] Built PrimeCert.Meta.PrimeCert (1.9s)
✔ [4203/4205] Built PrimeCert.Meta.SmallPrime (1.1s)
✔ [4204/4207] Built PrimeCert.PredMod (500ms)
✔ [4205/4211] Built PrimeCert.PowMod (1.5s)
✔ [4208/4220] Built PrimeCert.Pocklington (2.7s)
✔ [4210/4220] Built PrimeCert.SmallPrimes (2.1s)
✔ [4211/4222] Built PrimeCert.Pocklington3 (4.3s)
✔ [4212/4222] Built PrimeCert.Wieferich (2.2s)
⚠ [4213/4225] Built PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting (18s)
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`
✔ [4215/4225] Built PrimeCert (1.7s)
✔ [4217/4225] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.AbsMax (3.9s)
✖ [4218/4225] Building PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers (6.1s)
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
✔ [4219/4259] Built PrimeNumberTheoremAnd.IEANTN.PrimeTables (6.3s)
✔ [4223/4261] Built PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative (4.9s)
✔ [4225/4261] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanProductBound (1.6s)
✔ [4226/4261] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.BorelCaratheodory (2.3s)
✔ [4227/4261] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial (1.6s)
✔ [4228/4261] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFunctionalEquation (1.7s)
✔ [4229/4261] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Basic (1.6s)
✔ [4230/4261] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Trigonometric (1.4s)
✔ [4231/4261] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.IntegralBounds (1.8s)
✔ [4232/4261] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.GammaBounds (3.1s)
✔ [4233/4261] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.GammaStirlingAux (1.8s)
✔ [4234/4261] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Real (1.7s)
✔ [4235/4261] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta (2.4s)
✔ [4236/4261] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Convex (2.8s)
✔ [4237/4261] Built PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Integral.IntegrableOn (1.5s)
✔ [4238/4261] Built PrimeNumberTheoremAnd.Mathlib.Algebra.Order.Floor.Ring (1.1s)
✔ [4239/4261] Built PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (1.5s)
✔ [4242/4276] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation (1.8s)
✔ [4245/4276] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly (7.4s)
✔ [4246/4276] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.CompletedXi (1.8s)
✔ [4247/4276] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds (5.2s)
✔ [4248/4276] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (1.8s)
✔ [4251/4276] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.DigammaSeries (16s)
✔ [4252/4276] Built PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Cauchy (1.2s)
✔ [4253/4276] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev (3.3s)
⚠ [4254/4276] Built PrimeNumberTheoremAnd.IwaniecKowalskiCh1 (9.6s)
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`
✔ [4259/4283] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly (2.2s)
✔ [4260/4283] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly.Growth (3.7s)
✔ [4261/4283] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelKernel (3.0s)
✔ [4262/4283] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaValues (2.4s)
⚠ [4263/4283] Built PrimeNumberTheoremAnd.LaplaceInversion (9.8s)
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`
✔ [4265/4283] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CauchyIntegral (1.7s)
⚠ [4266/4283] Built PrimeNumberTheoremAnd.PerronFormula (9.4s)
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.Mathlib.Analysis.Complex.CartanBound (4.8s)
✔ [4268/4283] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaPartialSum (2.6s)
✔ [4270/4283] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanMajorantBound (10s)
✔ [4271/4283] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanInverseFactorBound (2.4s)
✔ [4272/4283] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelContinuation (2.5s)
✔ [4273/4283] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalDecomposition (1.4s)
✔ [4274/4283] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Growth (4.5s)
✔ [4275/4283] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaConvexity (2.2s)
✔ [4276/4283] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order (2.1s)
✔ [4277/4283] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaStripBound (1.7s)
✔ [4278/4283] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder (13s)
✔ [4279/4283] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaHadamard (2.0s)
✔ [4280/4283] Built PrimeNumberTheoremAnd.IEANTN.KadiriEq13 (5.7s)
Some required targets logged failures:
- PrimeNumberTheoremAnd.IEANTN.Mertens
- PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers

error: build failed

lake build :blueprint

✔ [16/35] Built Batteries.Lean.NameMapAttribute:c.o (1.6s)
✔ [17/35] Built Architect.Basic:c.o (902ms)
✔ [18/35] Built Architect.Command:c.o (294ms)
✔ [19/35] Built Architect.Content:c.o (219ms)
✔ [20/35] Built Architect.Attribute:c.o (958ms)
✔ [21/35] Built Architect.CollectUsed:c.o (158ms)
✔ [22/35] Built Architect.Tactic:c.o (785ms)
✔ [23/35] Built Architect.Output:c.o (2.3s)
✔ [24/35] Built Architect.Load:c.o (208ms)
✔ [25/35] Built Architect:c.o (80ms)
✔ [27/35] Built Cli.Basic:c.o (3.1s)
✔ [30/35] Built Cli.Extensions:c.o (498ms)
✔ [31/35] Built Cli:c.o (69ms)
✔ [32/35] Built Main (2.1s)
✔ [33/35] Built Main:c.o (294ms)
✔ [34/41] Built extract_blueprint:exe (6.4s)
✔ [2103/2110] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Auxiliary:blueprint (22s)
✔ [3035/3041] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Sobolev:blueprint (56s)
✔ [3055/3061] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Fourier:blueprint (7.4s)
✔ [3084/3097] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Defs:blueprint (46s)
✔ [3575/3585] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic:blueprint (2.8s)
✔ [3576/3585] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Rectangle:blueprint (2.6s)
✔ [3581/3593] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaConj:blueprint (15s)
✔ [3582/3593] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Tactic.AdditiveCombination:blueprint (1.4s)
✔ [3586/3598] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions:blueprint (20s)
✔ [3588/3598] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMaclaurin:blueprint (3.1s)
✔ [3596/3608] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ResidueCalcOnRectangles:blueprint (14s)
✔ [3599/3608] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds:blueprint (2.7s)
✔ [3600/3608] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Norm:blueprint (1.7s)
✔ [3602/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (64s)
✔ [3610/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorSupport:blueprint (13s)
✔ [3611/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit:blueprint (2.7s)
✔ [3613/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor:blueprint (3.3s)
✔ [3616/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalProduct:blueprint (2.5s)
✔ [3618/3638] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Annulus:blueprint (1.6s)
✔ [3619/3640] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorIndex:blueprint (2.4s)
✔ [3622/3642] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorConvergence:blueprint (2.4s)
✔ [3623/3642] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorUnits:blueprint (2.4s)
✔ [3626/3645] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorFiber:blueprint (2.5s)
✔ [3630/3648] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement:blueprint (2.4s)
✔ [3634/3648] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorPartialProductFactor:blueprint (2.4s)
✔ [3639/3653] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientConvergence:blueprint (2.4s)
✔ [3642/3655] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientRemovable:blueprint (2.4s)
✔ [3647/3655] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor:blueprint (2.4s)
✔ [3650/3658] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization:blueprint (2.5s)
✔ [3666/3694] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Exp:blueprint (1.9s)
✔ [3667/3694] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorHolomorphic:blueprint (2.4s)
✔ [3668/3694] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic:blueprint (1.0s)
✔ [3673/3696] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.PosLog:blueprint (1.9s)
✔ [3675/3696] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MellinCalculus:blueprint (30s)
✔ [3676/3696] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support:blueprint (978ms)
✔ [3681/3699] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth:blueprint (1.0s)
✔ [3682/3699] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.SmoothExistence:blueprint (5.2s)
ℹ [3683/3699] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3686/3701] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (77s)
✔ [3693/3701] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic:blueprint (9.1s)
✔ [3696/3712] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Growth:blueprint (2.4s)
✔ [3699/3724] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability:blueprint (2.9s)
✔ [3703/3726] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Backlund.ZeroCountCrude:blueprint (18s)
✔ [3706/3726] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics:blueprint (7.1s)
✔ [3711/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults:blueprint (3.9s)
⚠ [3715/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`
✔ [3716/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic:blueprint (2.5s)
✔ [3719/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (58s)
✔ [3721/3727] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg:blueprint (2.4s)
✔ [3723/3728] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (7.5s)
✔ [3724/3728] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds:blueprint (9.0s)
✔ [3726/3728] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BrunTitchmarsh:blueprint (2.5s)
⚠ [3849/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 (43s)
⚠ [3853/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`
✔ [3854/3867] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Consequences:blueprint (43s)
⚠ [3966/3982] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3969/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.GeneralMeromorphic:blueprint (5.8s)
✔ [3970/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HadamardFactorization:blueprint (1.3s)
✔ [3971/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HoffsteinLockhart:blueprint (3.7s)
✔ [3972/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KLN:blueprint (4.0s)
✔ [3973/3983] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta:blueprint (3.5s)
✔ [3976/3984] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (6.4s)
✖ [3978/3984] Building PrimeNumberTheoremAnd.IEANTN.Mertens (37s)
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/Mertens.lean -o /apx/source/.lake/build/lib/lean/PrimeNumberTheoremAnd/IEANTN/Mertens.olean -i /apx/source/.lake/build/lib/lean/PrimeNumberTheoremAnd/IEANTN/Mertens.ilean -c /apx/source/.lake/build/ir/PrimeNumberTheoremAnd/IEANTN/Mertens.c --setup /apx/source/.lake/build/ir/PrimeNumberTheoremAnd/IEANTN/Mertens.setup.json --json
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:1152: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`
error: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1246:4: Type mismatch: After simplification, term
  Summable.neg this
 has type
  @Summable ℝ Nat.Primes Real.instAddCommGroup.toAddCommMonoid PseudoMetricSpace.toUniformSpace.toTopologicalSpace
    (fun b ↦ -log (1 + -z b)) (SummationFilter.unconditional Nat.Primes)
but is expected to have type
  @Summable ℝ Nat.Primes Real.instAddCommMonoid PseudoMetricSpace.toUniformSpace.toTopologicalSpace
    (fun p ↦ -log (1 - z p)) (SummationFilter.unconditional Nat.Primes)
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1305:16: declaration uses `sorry`
error: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1332:2: `grind` failed
case grind.2
s : ℝ
hs : 1 < s
h :
  ¬(s - 1) *
        ∫ (a : ℝ) in Set.Ioi 1,
          (∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                1 -
              log (log 2)) *
            a ^ (-s) ∂MeasureTheory.volume =
      ∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume + 1 -
        log (log 2)
h_1 : ¬-s + 1 = 0
⊢ False
[grind] Goal diagnostics
  [facts] Asserted facts
    [prop] 1 < s
    [prop] ¬(s - 1) *
              ∫ (a : ℝ) in Set.Ioi 1,
                (∫ (t : ℝ) in Set.Ioi 2,
                        (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                      1 -
                    log (log 2)) *
                  a ^ (-s) ∂MeasureTheory.volume =
            ∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                1 -
              log (log 2)
    [prop] ∫ (a : ℝ) in Set.Ioi 1,
            (∫ (t : ℝ) in Set.Ioi 2,
                    (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                  1 -
                log (log 2)) *
              a ^ (-s) ∂MeasureTheory.volume =
          (∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                1 -
              log (log 2)) *
            ∫ (x : ℝ) in Set.Ioi 1, x ^ (-s) ∂MeasureTheory.volume
    [prop] -s < -1 → 0 < 1 → ∫ (x : ℝ) in Set.Ioi 1, x ^ (-s) ∂MeasureTheory.volume = -1 ^ (-s + 1) * (-s + 1)⁻¹
    [prop] if -s + 1 = 0 then (-s + 1)⁻¹ = 0 else (-s + 1) * (-s + 1)⁻¹ = 1
    [prop] 1 ^ (-s + 1) = 1
    [prop] ¬-s + 1 = 0
  [eqc] True propositions
    [prop] (-s + 1) * (-s + 1)⁻¹ = 1
    [prop] 1 < s
    [prop] if -s + 1 = 0 then (-s + 1)⁻¹ = 0 else (-s + 1) * (-s + 1)⁻¹ = 1
    [prop] ∫ (x : ℝ) in Set.Ioi 1, x ^ (-s) ∂MeasureTheory.volume = -1 ^ (-s + 1) * (-s + 1)⁻¹
    [prop] -s < -1
    [prop] 0 < 1
    [prop] -s < -1 → 0 < 1 → ∫ (x : ℝ) in Set.Ioi 1, x ^ (-s) ∂MeasureTheory.volume = -1 ^ (-s + 1) * (-s + 1)⁻¹
    [prop] 0 < 1 → ∫ (x : ℝ) in Set.Ioi 1, x ^ (-s) ∂MeasureTheory.volume = -1 ^ (-s + 1) * (-s + 1)⁻¹
  [eqc] False propositions
    [prop] -s + 1 = 0
    [prop] (s - 1) *
            ∫ (a : ℝ) in Set.Ioi 1,
              (∫ (t : ℝ) in Set.Ioi 2,
                      (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                    1 -
                  log (log 2)) *
                a ^ (-s) ∂MeasureTheory.volume =
          ∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
              1 -
            log (log 2)
  [eqc] Equivalence classes
    [eqc] {1,
        (-s + 1) * (-s + 1)⁻¹,
        ((s - 1) *
              ∫ (a : ℝ) in Set.Ioi 1,
                (∫ (t : ℝ) in Set.Ioi 2,
                        (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                      1 -
                    log (log 2)) *
                  a ^ (-s) ∂MeasureTheory.volume -
            (∫ (t : ℝ) in Set.Ioi 2,
                  (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                1 -
              log (log 2))) *
          ((s - 1) *
                ∫ (a : ℝ) in Set.Ioi 1,
                  (∫ (t : ℝ) in Set.Ioi 2,
                          (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                        1 -
                      log (log 2)) *
                    a ^ (-s) ∂MeasureTheory.volume -
              (∫ (t : ℝ) in Set.Ioi 2,
                    (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                  1 -
                log (log 2)))⁻¹,
        1 ^ (-s + 1)}
    [eqc] {(∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
              1 -
            log (log 2)) *
          ∫ (x : ℝ) in Set.Ioi 1, x ^ (-s) ∂MeasureTheory.volume,
        ∫ (a : ℝ) in Set.Ioi 1,
          (∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                1 -
              log (log 2)) *
            a ^ (-s) ∂MeasureTheory.volume}
    [eqc] {-1, -1 ^ (-s + 1)}
    [eqc] {-1 ^ (-s + 1) * (-s + 1)⁻¹, ∫ (x : ℝ) in Set.Ioi 1, x ^ (-s) ∂MeasureTheory.volume}
  [cases] Case analyses
    [cases] [2/2]: if -s + 1 = 0 then (-s + 1)⁻¹ = 0 else (-s + 1) * (-s + 1)⁻¹ = 1
      [cases] source: E-matching `@integral_Ioi_rpow_of_lt (-s)`
  [ematch] E-matching patterns
    [thm] MeasureTheory.integral_const_mul γ
              (· ^
                (-s)): [@MeasureTheory.integral `[ℝ] `[ℝ] `[NonUnitalNormedRing.toNormedAddCommGroup] `[NormedAlgebra.toNormedSpace
           ℝ] #1 #0 `[fun a ↦
           (∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                 1 -
               log (log 2)) *
             a ^ (-s)]]
    [thm] @integral_Ioi_rpow_of_lt
              (-s): [@MeasureTheory.integral `[ℝ] `[ℝ] `[normedAddCommGroup] `[RCLike.toInnerProductSpaceReal.toNormedSpace] `[measurableSpace] (@MeasureTheory.Measure.restrict `[ℝ] `[measurableSpace] `[MeasureTheory.volume] (@Set.Ioi `[ℝ] `[instPreorder] #1)) `[fun
             x ↦
           x ^ (-s)]]
    [thm] one_rpow: [@HPow.hPow `[ℝ] `[ℝ] `[ℝ] `[instHPow] `[1] #0]
    [thm] Nat.pow_pos: [@HPow.hPow `[ℕ] `[ℕ] `[ℕ] `[instHPow] #2 #1]
    [thm] Nat.div_pow_of_pos: [@HPow.hPow `[ℕ] `[ℕ] `[ℕ] `[instHPow] #2 #1]
  [linarith] Linarith assignment for `ℝ`
    [assign] s := 2
    [assign] log (log 2) := 0
    [assign] log 2 := 9
    [assign] ∫ (a : ℝ) in Set.Ioi 1,
          (∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                1 -
              log (log 2)) *
            a ^ (-s) ∂MeasureTheory.volume := 0
    [assign] ∫ (t : ℝ) in Set.Ioi 2,
          (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume := 0
    [assign] ∫ (a : ℝ) in Set.Ioi 1,
          (∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                1 -
              log (log 2)) *
            a ^ (-s) ∂MeasureTheory.volume := 0
    [assign] ∫ (x : ℝ) in Set.Ioi 1, x ^ (-s) ∂MeasureTheory.volume := 20
    [assign] 「1 ^ (-s + 1)」 := 1
    [assign] ∫ (x : ℝ) in Set.Ioi 1, x ^ (-s) ∂MeasureTheory.volume := 0
  [ring] Ring `ℝ`
    [basis] Basis
      [_] (s *
                          ∫ (a : ℝ) in Set.Ioi 1,
                            (∫ (t : ℝ) in Set.Ioi 2,
                                    (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                  1 -
                                log (log 2)) *
                              a ^ (-s) ∂MeasureTheory.volume) *
                        ((s - 1) *
                              ∫ (a : ℝ) in Set.Ioi 1,
                                (∫ (t : ℝ) in Set.Ioi 2,
                                        (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) *
                                          (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                      1 -
                                    log (log 2)) *
                                  a ^ (-s) ∂MeasureTheory.volume -
                            (∫ (t : ℝ) in Set.Ioi 2,
                                  (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                1 -
                              log (log 2)))⁻¹ +
                      -1 *
                        ((∫ (a : ℝ) in Set.Ioi 1,
                            (∫ (t : ℝ) in Set.Ioi 2,
                                    (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                  1 -
                                log (log 2)) *
                              a ^ (-s) ∂MeasureTheory.volume) *
                          ((s - 1) *
                                ∫ (a : ℝ) in Set.Ioi 1,
                                  (∫ (t : ℝ) in Set.Ioi 2,
                                          (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) *
                                            (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                        1 -
                                      log (log 2)) *
                                    a ^ (-s) ∂MeasureTheory.volume -
                              (∫ (t : ℝ) in Set.Ioi 2,
                                    (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                  1 -
                                log (log 2)))⁻¹) +
                    -1 *
                      ((∫ (t : ℝ) in Set.Ioi 2,
                          (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume) *
                        ((s - 1) *
                              ∫ (a : ℝ) in Set.Ioi 1,
                                (∫ (t : ℝ) in Set.Ioi 2,
                                        (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) *
                                          (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                      1 -
                                    log (log 2)) *
                                  a ^ (-s) ∂MeasureTheory.volume -
                            (∫ (t : ℝ) in Set.Ioi 2,
                                  (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                1 -
                              log (log 2)))⁻¹) +
                  log (log 2) *
                    ((s - 1) *
                          ∫ (a : ℝ) in Set.Ioi 1,
                            (∫ (t : ℝ) in Set.Ioi 2,
                                    (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                  1 -
                                log (log 2)) *
                              a ^ (-s) ∂MeasureTheory.volume -
                        (∫ (t : ℝ) in Set.Ioi 2,
                              (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                            1 -
                          log (log 2)))⁻¹ +
                -1 *
                  ((s - 1) *
                        ∫ (a : ℝ) in Set.Ioi 1,
                          (∫ (t : ℝ) in Set.Ioi 2,
                                  (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                1 -
                              log (log 2)) *
                            a ^ (-s) ∂MeasureTheory.volume -
                      (∫ (t : ℝ) in Set.Ioi 2,
                            (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                          1 -
                        log (log 2)))⁻¹ +
              -1 =
            0
      [_] (∫ (t : ℝ) in Set.Ioi 2, (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume) *
                        ((s - 1) *
                              ∫ (a : ℝ) in Set.Ioi 1,
                                (∫ (t : ℝ) in Set.Ioi 2,
                                        (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) *
                                          (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                      1 -
                                    log (log 2)) *
                                  a ^ (-s) ∂MeasureTheory.volume -
                            (∫ (t : ℝ) in Set.Ioi 2,
                                  (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                1 -
                              log (log 2)))⁻¹ *
                      (-s + 1)⁻¹ +
                    -1 *
                      (log (log 2) *
                          ((s - 1) *
                                ∫ (a : ℝ) in Set.Ioi 1,
                                  (∫ (t : ℝ) in Set.Ioi 2,
                                          (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) *
                                            (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                        1 -
                                      log (log 2)) *
                                    a ^ (-s) ∂MeasureTheory.volume -
                              (∫ (t : ℝ) in Set.Ioi 2,
                                    (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                  1 -
                                log (log 2)))⁻¹ *
                        (-s + 1)⁻¹) +
                  (∫ (a : ℝ) in Set.Ioi 1,
                      (∫ (t : ℝ) in Set.Ioi 2,
                              (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                            1 -
                          log (log 2)) *
                        a ^ (-s) ∂MeasureTheory.volume) *
                    ((s - 1) *
                          ∫ (a : ℝ) in Set.Ioi 1,
                            (∫ (t : ℝ) in Set.Ioi 2,
                                    (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                  1 -
                                log (log 2)) *
                              a ^ (-s) ∂MeasureTheory.volume -
                        (∫ (t : ℝ) in Set.Ioi 2,
                              (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                            1 -
                          log (log 2)))⁻¹ +
                ((s - 1) *
                        ∫ (a : ℝ) in Set.Ioi 1,
                          (∫ (t : ℝ) in Set.Ioi 2,
                                  (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                                1 -
                              log (log 2)) *
                            a ^ (-s) ∂MeasureTheory.volume -
                      (∫ (t : ℝ) in Set.Ioi 2,
                            (∑ x ∈ Ioc 0 ⌊t⌋₊, Λ x * (↑x)⁻¹ - log t) * (t * log t ^ 2)⁻¹ ∂MeasureTheory.volume +
                          1 -
                        log (log 2)))⁻¹ *
                  (-s + 1)⁻¹ +
              (-s + 1)⁻¹ =
            0
      [_] s * (-s + 1)⁻¹ + -1 * (-s + 1)⁻¹ + 1 = 0
      [_] 1 ^ (-s + 1) + -1 = 0
[grind] Diagnostics
  [thm] E-Matching instances
    [thm] extra_0 ↦ 1
    [thm] extra_1 ↦ 1
    [thm] one_rpow ↦ 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1799: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:1950: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:1987: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:2249: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:2267: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`
error: Lean exited with code 1
✔ [3979/3984] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv:blueprint (2.1s)
✔ [3981/3987] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMascheroniBounds:blueprint (9.6s)
✔ [4043/4064] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (2.9s)
⚠ [4052/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`
✔ [4054/4067] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries:blueprint (2.1s)
✔ [4056/4068] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PVIdentity:blueprint (2.7s)
✔ [4063/4070] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Li2Bounds:blueprint (11s)
✔ [4064/4070] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LiSeries:blueprint (3.6s)
✔ [4204/4217] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables:blueprint (2.5s)
✔ [4206/4217] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables:blueprint (7.3s)
✔ [4210/4272] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (8.2s)
✔ [4283/4294] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables:blueprint (4.1s)
⚠ [4284/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`
✔ [4288/4301] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP:blueprint (3.7s)
⚠ [4292/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`
✔ [4294/4301] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (21s)
ℹ [4296/4301] 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.
✔ [4299/4306] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations:blueprint (8.4s)
✔ [4348/4353] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Tactic.Simprocs:blueprint (1.2s)
⚠ [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 (5.3s)
✖ [4370/4384] Building PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers (9.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
✔ [4371/4452] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeTables:blueprint (2.4s)
✔ [4376/4452] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.AbsMax:blueprint (4.1s)
✔ [4389/4481] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative:blueprint (4.4s)
✔ [4400/4481] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanProductBound:blueprint (1.9s)
✔ [4401/4481] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.BorelCaratheodory:blueprint (2.4s)
✔ [4403/4481] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial:blueprint (2.0s)
✔ [4404/4481] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFunctionalEquation:blueprint (2.0s)
✔ [4406/4481] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Basic:blueprint (1.8s)
✔ [4407/4481] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Trigonometric:blueprint (1.6s)
✔ [4408/4481] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.IntegralBounds:blueprint (2.3s)
✔ [4409/4481] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.GammaBounds:blueprint (2.5s)
✔ [4410/4481] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.GammaStirlingAux:blueprint (2.3s)
✔ [4412/4481] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Real:blueprint (1.0s)
✔ [4413/4481] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta:blueprint (4.5s)
✔ [4414/4481] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Convex:blueprint (1.8s)
✔ [4415/4481] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Integral.IntegrableOn:blueprint (2.2s)
✔ [4420/4491] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Algebra.Order.Floor.Ring:blueprint (1.5s)
✔ [4421/4491] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic:blueprint (2.2s)
✔ [4422/4491] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation:blueprint (2.4s)
⚠ [4428/4491] 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`
✔ [4435/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly:blueprint (2.7s)
✔ [4437/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.CompletedXi:blueprint (2.5s)
✔ [4438/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds:blueprint (2.4s)
✔ [4439/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.ImproperIntegrals:blueprint (2.3s)
✔ [4442/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.DigammaSeries:blueprint (2.4s)
✔ [4443/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Cauchy:blueprint (1.4s)
⚠ [4444/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`
✔ [4445/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev:blueprint (2.4s)
✔ [4447/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IwaniecKowalskiCh1:blueprint (62s)
✔ [4448/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly:blueprint (3.5s)
⚠ [4451/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`
✔ [4455/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly.Growth:blueprint (3.3s)
✔ [4456/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelKernel:blueprint (4.6s)
✔ [4458/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaValues:blueprint (4.3s)
✔ [4459/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.LaplaceInversion:blueprint (2.5s)
✔ [4461/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CauchyIntegral:blueprint (2.3s)
✔ [4462/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.PerronFormula:blueprint (29s)
✔ [4463/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound:blueprint (4.1s)
✔ [4466/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaPartialSum:blueprint (3.3s)
✔ [4469/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanInverseFactorBound:blueprint (2.4s)
✔ [4470/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanMajorantBound:blueprint (3.1s)
✔ [4472/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelContinuation:blueprint (3.3s)
✔ [4474/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalDecomposition:blueprint (2.6s)
✔ [4475/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Growth:blueprint (3.3s)
✔ [4477/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaConvexity:blueprint (4.3s)
✔ [4479/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order:blueprint (2.3s)
✔ [4480/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaStripBound:blueprint (2.8s)
✔ [4482/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder:blueprint (3.8s)
✔ [4484/4492] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaHadamard:blueprint (2.8s)
✔ [4486/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriEq13:blueprint (12s)
Some required targets logged failures:
- PrimeNumberTheoremAnd.IEANTN.Mertens
- PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers

error: build failed