Run 1037

git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-1334-source

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

git checkout debe0878e45d9c0b482c66aa4b555b57237dcbf5

Note: switching to 'debe0878e45d9c0b482c66aa4b555b57237dcbf5'.

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 debe087 Lower norm square CTheta route

lake exe cache get

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

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

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 16 file(s) [attempted 16/8459 = 0%, 11 KB/s], Decompressed: 13
Downloaded: 42 file(s) [attempted 42/8459 = 0%, 80 KB/s], Decompressed: 35
Downloaded: 72 file(s) [attempted 72/8459 = 0%, 45 KB/s], Decompressed: 68
Downloaded: 98 file(s) [attempted 98/8459 = 1%, 94 KB/s], Decompressed: 93
Downloaded: 134 file(s) [attempted 134/8459 = 1%, 60 KB/s], Decompressed: 127
Downloaded: 172 file(s) [attempted 172/8459 = 2%, 111 KB/s], Decompressed: 158
Downloaded: 203 file(s) [attempted 203/8459 = 2%, 316 KB/s], Decompressed: 199
Downloaded: 234 file(s) [attempted 234/8459 = 2%, 568 KB/s], Decompressed: 230
Downloaded: 271 file(s) [attempted 271/8459 = 3%, 679 KB/s], Decompressed: 268
Downloaded: 312 file(s) [attempted 312/8459 = 3%, 527 KB/s], Decompressed: 309
Downloaded: 353 file(s) [attempted 353/8459 = 4%, 83 KB/s], Decompressed: 347
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 127 KB/s], Decompressed: 388
Downloaded: 432 file(s) [attempted 432/8459 = 5%, 281 KB/s], Decompressed: 425
Downloaded: 470 file(s) [attempted 470/8459 = 5%, 269 KB/s], Decompressed: 463
Downloaded: 508 file(s) [attempted 508/8459 = 6%, 648 KB/s], Decompressed: 477
Downloaded: 549 file(s) [attempted 549/8459 = 6%, 315 KB/s], Decompressed: 545
Downloaded: 593 file(s) [attempted 593/8459 = 7%, 271 KB/s], Decompressed: 583
Downloaded: 640 file(s) [attempted 640/8459 = 7%, 260 KB/s], Decompressed: 631
Downloaded: 679 file(s) [attempted 679/8459 = 8%, 105 KB/s], Decompressed: 675
Downloaded: 723 file(s) [attempted 723/8459 = 8%, 241 KB/s], Decompressed: 713
Downloaded: 758 file(s) [attempted 758/8459 = 8%, 55 KB/s], Decompressed: 754
Downloaded: 799 file(s) [attempted 799/8459 = 9%, 770 KB/s], Decompressed: 792
Downloaded: 836 file(s) [attempted 836/8459 = 9%, 222 KB/s], Decompressed: 826
Downloaded: 882 file(s) [attempted 882/8459 = 10%, 300 KB/s], Decompressed: 874
Downloaded: 919 file(s) [attempted 919/8459 = 10%, 583 KB/s], Decompressed: 915
Downloaded: 956 file(s) [attempted 956/8459 = 11%, 884 KB/s], Decompressed: 949
Downloaded: 999 file(s) [attempted 999/8459 = 11%, 313 KB/s], Decompressed: 991
Downloaded: 1038 file(s) [attempted 1038/8459 = 12%, 772 KB/s], Decompressed: 1032
Downloaded: 1086 file(s) [attempted 1086/8459 = 12%, 88 KB/s], Decompressed: 1085
Downloaded: 1127 file(s) [attempted 1127/8459 = 13%, 294 KB/s], Decompressed: 1124
Downloaded: 1165 file(s) [attempted 1165/8459 = 13%, 1780 KB/s], Decompressed: 1151
Downloaded: 1206 file(s) [attempted 1206/8459 = 14%, 1046 KB/s], Decompressed: 1203
Downloaded: 1244 file(s) [attempted 1244/8459 = 14%, 1138 KB/s], Decompressed: 1240
Downloaded: 1290 file(s) [attempted 1290/8459 = 15%, 179 KB/s], Decompressed: 1281
Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 302 KB/s], Decompressed: 1323
Downloaded: 1370 file(s) [attempted 1370/8459 = 16%, 238 KB/s], Decompressed: 1364
Downloaded: 1412 file(s) [attempted 1412/8459 = 16%, 236 KB/s], Decompressed: 1398
Downloaded: 1449 file(s) [attempted 1449/8459 = 17%, 743 KB/s], Decompressed: 1442
Downloaded: 1490 file(s) [attempted 1490/8459 = 17%, 2154 KB/s], Decompressed: 1487
Downloaded: 1538 file(s) [attempted 1538/8459 = 18%, 495 KB/s], Decompressed: 1535
Downloaded: 1586 file(s) [attempted 1586/8459 = 18%, 343 KB/s], Decompressed: 1572
Downloaded: 1620 file(s) [attempted 1620/8459 = 19%, 868 KB/s], Decompressed: 1603
Downloaded: 1664 file(s) [attempted 1664/8459 = 19%, 153 KB/s], Decompressed: 1658
Downloaded: 1702 file(s) [attempted 1702/8459 = 20%, 131 KB/s], Decompressed: 1696
Downloaded: 1743 file(s) [attempted 1743/8459 = 20%, 92 KB/s], Decompressed: 1740
Downloaded: 1785 file(s) [attempted 1785/8459 = 21%, 75 KB/s], Decompressed: 1778
Downloaded: 1826 file(s) [attempted 1826/8459 = 21%, 267 KB/s], Decompressed: 1822
Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 1505 KB/s], Decompressed: 1860
Downloaded: 1908 file(s) [attempted 1908/8459 = 22%, 343 KB/s], Decompressed: 1904
Downloaded: 1949 file(s) [attempted 1949/8459 = 23%, 836 KB/s], Decompressed: 1945
Downloaded: 1984 file(s) [attempted 1984/8459 = 23%, 80 KB/s], Decompressed: 1976
Downloaded: 2028 file(s) [attempted 2028/8459 = 23%, 520 KB/s], Decompressed: 2024
Downloaded: 2072 file(s) [attempted 2072/8459 = 24%, 40 KB/s], Decompressed: 2069
Downloaded: 2112 file(s) [attempted 2112/8459 = 24%, 371 KB/s], Decompressed: 2106
Downloaded: 2154 file(s) [attempted 2154/8459 = 25%, 175 KB/s], Decompressed: 2147
Downloaded: 2189 file(s) [attempted 2189/8459 = 25%, 438 KB/s], Decompressed: 2185
Downloaded: 2233 file(s) [attempted 2233/8459 = 26%, 114 KB/s], Decompressed: 2229
Downloaded: 2281 file(s) [attempted 2281/8459 = 26%, 369 KB/s], Decompressed: 2277
Downloaded: 2322 file(s) [attempted 2322/8459 = 27%, 84 KB/s], Decompressed: 2320
Downloaded: 2363 file(s) [attempted 2363/8459 = 27%, 149 KB/s], Decompressed: 2353
Downloaded: 2404 file(s) [attempted 2404/8459 = 28%, 472 KB/s], Decompressed: 2401
Downloaded: 2442 file(s) [attempted 2442/8459 = 28%, 268 KB/s], Decompressed: 2438
Downloaded: 2480 file(s) [attempted 2480/8459 = 29%, 31 KB/s], Decompressed: 2476
Downloaded: 2524 file(s) [attempted 2524/8459 = 29%, 260 KB/s], Decompressed: 2520
Downloaded: 2570 file(s) [attempted 2570/8459 = 30%, 454 KB/s], Decompressed: 2558
Downloaded: 2603 file(s) [attempted 2603/8459 = 30%, 626 KB/s], Decompressed: 2599
Downloaded: 2640 file(s) [attempted 2640/8459 = 31%, 765 KB/s], Decompressed: 2635
Downloaded: 2688 file(s) [attempted 2688/8459 = 31%, 181 KB/s], Decompressed: 2681
Downloaded: 2729 file(s) [attempted 2729/8459 = 32%, 168 KB/s], Decompressed: 2722
Downloaded: 2770 file(s) [attempted 2770/8459 = 32%, 256 KB/s], Decompressed: 2760
Downloaded: 2808 file(s) [attempted 2808/8459 = 33%, 107 KB/s], Decompressed: 2804
Downloaded: 2852 file(s) [attempted 2852/8459 = 33%, 133 KB/s], Decompressed: 2845
Downloaded: 2897 file(s) [attempted 2897/8459 = 34%, 82 KB/s], Decompressed: 2890
Downloaded: 2938 file(s) [attempted 2938/8459 = 34%, 273 KB/s], Decompressed: 2907
Downloaded: 2982 file(s) [attempted 2982/8459 = 35%, 24 KB/s], Decompressed: 2976
Downloaded: 3022 file(s) [attempted 3022/8459 = 35%, 144 KB/s], Decompressed: 3013
Downloaded: 3054 file(s) [attempted 3054/8459 = 36%, 408 KB/s], Decompressed: 3051
Downloaded: 3099 file(s) [attempted 3099/8459 = 36%, 503 KB/s], Decompressed: 3096
Downloaded: 3147 file(s) [attempted 3147/8459 = 37%, 100 KB/s], Decompressed: 3143
Downloaded: 3193 file(s) [attempted 3193/8459 = 37%, 443 KB/s], Decompressed: 3190
Downloaded: 3233 file(s) [attempted 3233/8459 = 38%, 116 KB/s], Decompressed: 3225
Downloaded: 3270 file(s) [attempted 3270/8459 = 38%, 186 KB/s], Decompressed: 3249
Downloaded: 3311 file(s) [attempted 3311/8459 = 39%, 700 KB/s], Decompressed: 3280
Downloaded: 3355 file(s) [attempted 3355/8459 = 39%, 52 KB/s], Decompressed: 3352
Downloaded: 3396 file(s) [attempted 3396/8459 = 40%, 1164 KB/s], Decompressed: 3390
Downloaded: 3438 file(s) [attempted 3438/8459 = 40%, 894 KB/s], Decompressed: 3427
Downloaded: 3474 file(s) [attempted 3474/8459 = 41%, 852 KB/s], Decompressed: 3465
Downloaded: 3509 file(s) [attempted 3509/8459 = 41%, 587 KB/s], Decompressed: 3503
Downloaded: 3554 file(s) [attempted 3554/8459 = 42%, 201 KB/s], Decompressed: 3550
Downloaded: 3598 file(s) [attempted 3598/8459 = 42%, 190 KB/s], Decompressed: 3595
Downloaded: 3639 file(s) [attempted 3639/8459 = 43%, 124 KB/s], Decompressed: 3630
Downloaded: 3674 file(s) [attempted 3674/8459 = 43%, 78 KB/s], Decompressed: 3667
Downloaded: 3718 file(s) [attempted 3718/8459 = 43%, 88 KB/s], Decompressed: 3708
Downloaded: 3766 file(s) [attempted 3766/8459 = 44%, 675 KB/s], Decompressed: 3756
Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 450 KB/s], Decompressed: 3804
Downloaded: 3852 file(s) [attempted 3852/8459 = 45%, 106 KB/s], Decompressed: 3848
Downloaded: 3893 file(s) [attempted 3893/8459 = 46%, 592 KB/s], Decompressed: 3869
Downloaded: 3934 file(s) [attempted 3934/8459 = 46%, 96 KB/s], Decompressed: 3927
Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 312 KB/s], Decompressed: 3958
Downloaded: 4016 file(s) [attempted 4016/8459 = 47%, 47 KB/s], Decompressed: 4009
Downloaded: 4057 file(s) [attempted 4057/8459 = 47%, 2073 KB/s], Decompressed: 4054
Downloaded: 4098 file(s) [attempted 4098/8459 = 48%, 748 KB/s], Decompressed: 4057
Downloaded: 4139 file(s) [attempted 4139/8459 = 48%, 178 KB/s], Decompressed: 4057
Downloaded: 4180 file(s) [attempted 4180/8459 = 49%, 112 KB/s], Decompressed: 4149
Downloaded: 4221 file(s) [attempted 4221/8459 = 49%, 393 KB/s], Decompressed: 4214
Downloaded: 4262 file(s) [attempted 4262/8459 = 50%, 254 KB/s], Decompressed: 4252
Downloaded: 4299 file(s) [attempted 4299/8459 = 50%, 115 KB/s], Decompressed: 4293
Downloaded: 4341 file(s) [attempted 4341/8459 = 51%, 209 KB/s], Decompressed: 4334
Downloaded: 4382 file(s) [attempted 4382/8459 = 51%, 194 KB/s], Decompressed: 4379
Downloaded: 4427 file(s) [attempted 4427/8459 = 52%, 549 KB/s], Decompressed: 4416
Downloaded: 4464 file(s) [attempted 4464/8459 = 52%, 621 KB/s], Decompressed: 4461
Downloaded: 4506 file(s) [attempted 4506/8459 = 53%, 440 KB/s], Decompressed: 4502
Downloaded: 4546 file(s) [attempted 4546/8459 = 53%, 1291 KB/s], Decompressed: 4543
Downloaded: 4587 file(s) [attempted 4587/8459 = 54%, 608 KB/s], Decompressed: 4584
Downloaded: 4626 file(s) [attempted 4626/8459 = 54%, 1112 KB/s], Decompressed: 4618
Downloaded: 4670 file(s) [attempted 4670/8459 = 55%, 410 KB/s], Decompressed: 4666
Downloaded: 4711 file(s) [attempted 4711/8459 = 55%, 159 KB/s], Decompressed: 4707
Downloaded: 4753 file(s) [attempted 4753/8459 = 56%, 171 KB/s], Decompressed: 4748
Downloaded: 4793 file(s) [attempted 4793/8459 = 56%, 369 KB/s], Decompressed: 4789
Downloaded: 4831 file(s) [attempted 4831/8459 = 57%, 53 KB/s], Decompressed: 4827
Downloaded: 4871 file(s) [attempted 4871/8459 = 57%, 89 KB/s], Decompressed: 4868
Downloaded: 4913 file(s) [attempted 4913/8459 = 58%, 277 KB/s], Decompressed: 4909
Downloaded: 4957 file(s) [attempted 4957/8459 = 58%, 199 KB/s], Decompressed: 4954
Downloaded: 4998 file(s) [attempted 4998/8459 = 59%, 267 KB/s], Decompressed: 4995
Downloaded: 5039 file(s) [attempted 5039/8459 = 59%, 275 KB/s], Decompressed: 5036
Downloaded: 5087 file(s) [attempted 5087/8459 = 60%, 99 KB/s], Decompressed: 5080
Downloaded: 5128 file(s) [attempted 5128/8459 = 60%, 46 KB/s], Decompressed: 5121
Downloaded: 5166 file(s) [attempted 5166/8459 = 61%, 502 KB/s], Decompressed: 5162
Downloaded: 5210 file(s) [attempted 5210/8459 = 61%, 49 KB/s], Decompressed: 5207
Downloaded: 5248 file(s) [attempted 5248/8459 = 62%, 441 KB/s], Decompressed: 5241
Downloaded: 5289 file(s) [attempted 5289/8459 = 62%, 151 KB/s], Decompressed: 5286
Downloaded: 5334 file(s) [attempted 5334/8459 = 63%, 417 KB/s], Decompressed: 5323
Downloaded: 5371 file(s) [attempted 5371/8459 = 63%, 1126 KB/s], Decompressed: 5347
Downloaded: 5416 file(s) [attempted 5416/8459 = 64%, 324 KB/s], Decompressed: 5409
Downloaded: 5453 file(s) [attempted 5453/8459 = 64%, 172 KB/s], Decompressed: 5450
Downloaded: 5499 file(s) [attempted 5499/8459 = 65%, 70 KB/s], Decompressed: 5491
Downloaded: 5537 file(s) [attempted 5537/8459 = 65%, 170 KB/s], Decompressed: 5529
Downloaded: 5576 file(s) [attempted 5576/8459 = 65%, 1464 KB/s], Decompressed: 5573
Downloaded: 5624 file(s) [attempted 5624/8459 = 66%, 539 KB/s], Decompressed: 5618
Downloaded: 5665 file(s) [attempted 5665/8459 = 66%, 147 KB/s], Decompressed: 5659
Downloaded: 5707 file(s) [attempted 5707/8459 = 67%, 184 KB/s], Decompressed: 5696
Downloaded: 5744 file(s) [attempted 5744/8459 = 67%, 254 KB/s], Decompressed: 5737
Downloaded: 5782 file(s) [attempted 5782/8459 = 68%, 117 KB/s], Decompressed: 5778
Downloaded: 5826 file(s) [attempted 5826/8459 = 68%, 390 KB/s], Decompressed: 5819
Downloaded: 5874 file(s) [attempted 5874/8459 = 69%, 157 KB/s], Decompressed: 5867
Downloaded: 5922 file(s) [attempted 5922/8459 = 70%, 334 KB/s], Decompressed: 5915
Downloaded: 5963 file(s) [attempted 5963/8459 = 70%, 965 KB/s], Decompressed: 5956
Downloaded: 6001 file(s) [attempted 6001/8459 = 70%, 1120 KB/s], Decompressed: 5991
Downloaded: 6039 file(s) [attempted 6039/8459 = 71%, 496 KB/s], Decompressed: 6032
Downloaded: 6082 file(s) [attempted 6082/8459 = 71%, 230 KB/s], Decompressed: 6073
Downloaded: 6121 file(s) [attempted 6121/8459 = 72%, 191 KB/s], Decompressed: 6114
Downloaded: 6165 file(s) [attempted 6165/8459 = 72%, 206 KB/s], Decompressed: 6158
Downloaded: 6206 file(s) [attempted 6206/8459 = 73%, 43 KB/s], Decompressed: 6199
Downloaded: 6247 file(s) [attempted 6247/8459 = 73%, 32 KB/s], Decompressed: 6240
Downloaded: 6285 file(s) [attempted 6285/8459 = 74%, 54 KB/s], Decompressed: 6275
Downloaded: 6329 file(s) [attempted 6329/8459 = 74%, 114 KB/s], Decompressed: 6326
Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 495 KB/s], Decompressed: 6370
Downloaded: 6416 file(s) [attempted 6416/8459 = 75%, 51 KB/s], Decompressed: 6412
Downloaded: 6459 file(s) [attempted 6459/8459 = 76%, 648 KB/s], Decompressed: 6456
Downloaded: 6504 file(s) [attempted 6504/8459 = 76%, 434 KB/s], Decompressed: 6497
Downloaded: 6539 file(s) [attempted 6539/8459 = 77%, 211 KB/s], Decompressed: 6531
Downloaded: 6583 file(s) [attempted 6583/8459 = 77%, 364 KB/s], Decompressed: 6576
Downloaded: 6620 file(s) [attempted 6620/8459 = 78%, 290 KB/s], Decompressed: 6617
Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 208 KB/s], Decompressed: 6658
Downloaded: 6706 file(s) [attempted 6706/8459 = 79%, 80 KB/s], Decompressed: 6702
Downloaded: 6747 file(s) [attempted 6747/8459 = 79%, 715 KB/s], Decompressed: 6740
Downloaded: 6785 file(s) [attempted 6785/8459 = 80%, 79 KB/s], Decompressed: 6778
Downloaded: 6829 file(s) [attempted 6829/8459 = 80%, 332 KB/s], Decompressed: 6798
Downloaded: 6870 file(s) [attempted 6870/8459 = 81%, 222 KB/s], Decompressed: 6863
Downloaded: 6918 file(s) [attempted 6918/8459 = 81%, 34 KB/s], Decompressed: 6911
Downloaded: 6966 file(s) [attempted 6966/8459 = 82%, 198 KB/s], Decompressed: 6959
Downloaded: 7007 file(s) [attempted 7007/8459 = 82%, 166 KB/s], Decompressed: 7000
Downloaded: 7041 file(s) [attempted 7041/8459 = 83%, 23 KB/s], Decompressed: 7028
Downloaded: 7082 file(s) [attempted 7082/8459 = 83%, 43 KB/s], Decompressed: 7075
Downloaded: 7127 file(s) [attempted 7127/8459 = 84%, 32 KB/s], Decompressed: 7123
Downloaded: 7175 file(s) [attempted 7175/8459 = 84%, 317 KB/s], Decompressed: 7171
Downloaded: 7224 file(s) [attempted 7224/8459 = 85%, 460 KB/s], Decompressed: 7216
Downloaded: 7264 file(s) [attempted 7264/8459 = 85%, 129 KB/s], Decompressed: 7260
Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 2135 KB/s], Decompressed: 7291
Downloaded: 7341 file(s) [attempted 7341/8459 = 86%, 599 KB/s], Decompressed: 7332
Downloaded: 7380 file(s) [attempted 7380/8459 = 87%, 197 KB/s], Decompressed: 7377
Downloaded: 7421 file(s) [attempted 7421/8459 = 87%, 241 KB/s], Decompressed: 7418
Downloaded: 7464 file(s) [attempted 7464/8459 = 88%, 380 KB/s], Decompressed: 7455
Downloaded: 7500 file(s) [attempted 7500/8459 = 88%, 451 KB/s], Decompressed: 7486
Downloaded: 7536 file(s) [attempted 7536/8459 = 89%, 172 KB/s], Decompressed: 7527
Downloaded: 7575 file(s) [attempted 7575/8459 = 89%, 915 KB/s], Decompressed: 7565
Downloaded: 7616 file(s) [attempted 7616/8459 = 90%, 33 KB/s], Decompressed: 7613
Downloaded: 7664 file(s) [attempted 7664/8459 = 90%, 133 KB/s], Decompressed: 7657
Downloaded: 7705 file(s) [attempted 7705/8459 = 91%, 199 KB/s], Decompressed: 7698
Downloaded: 7753 file(s) [attempted 7753/8459 = 91%, 223 KB/s], Decompressed: 7746
Downloaded: 7794 file(s) [attempted 7794/8459 = 92%, 51 KB/s], Decompressed: 7787
Downloaded: 7832 file(s) [attempted 7832/8459 = 92%, 450 KB/s], Decompressed: 7825
Downloaded: 7873 file(s) [attempted 7873/8459 = 93%, 92 KB/s], Decompressed: 7866
Downloaded: 7910 file(s) [attempted 7910/8459 = 93%, 56 KB/s], Decompressed: 7908
Downloaded: 7953 file(s) [attempted 7953/8459 = 94%, 306 KB/s], Decompressed: 7948
Downloaded: 7996 file(s) [attempted 7996/8459 = 94%, 303 KB/s], Decompressed: 7993
Downloaded: 8037 file(s) [attempted 8037/8459 = 95%, 108 KB/s], Decompressed: 8027
Downloaded: 8072 file(s) [attempted 8072/8459 = 95%, 306 KB/s], Decompressed: 8068
Downloaded: 8109 file(s) [attempted 8109/8459 = 95%, 94 KB/s], Decompressed: 8106
Downloaded: 8157 file(s) [attempted 8157/8459 = 96%, 121 KB/s], Decompressed: 8153
Downloaded: 8205 file(s) [attempted 8205/8459 = 96%, 421 KB/s], Decompressed: 8198
Downloaded: 8243 file(s) [attempted 8243/8459 = 97%, 409 KB/s], Decompressed: 8236
Downloaded: 8283 file(s) [attempted 8283/8459 = 97%, 130 KB/s], Decompressed: 8260
Downloaded: 8321 file(s) [attempted 8321/8459 = 98%, 306 KB/s], Decompressed: 8314
Downloaded: 8362 file(s) [attempted 8362/8459 = 98%, 238 KB/s], Decompressed: 8359
Downloaded: 8403 file(s) [attempted 8403/8459 = 99%, 119 KB/s], Decompressed: 8400
Downloaded: 8448 file(s) [attempted 8448/8459 = 99%, 189 KB/s], Decompressed: 8441
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 189 KB/s], Decompressed: 8455

lake build

✔ [753/764] Built Iut.Foundations.RealLineCopy (11s)
✔ [754/764] Built Iut.Foundations.TransportDiagram (1.7s)
✔ [756/764] Built Iut.Foundations.IndeterminacyRelation (1.8s)
✔ [758/764] Built Iut.Foundations.RegionMeasure (1.7s)
✔ [760/764] Built Iut.Foundations.CommonTargetBound (1.7s)
✔ [762/764] Built Iut.Foundations.TransportedRegionFamily (1.6s)
✔ [763/779] Built Iut.Foundations.QualitativeData (2.2s)
✔ [3383/3392] Built Iut.Foundations.AlgorithmicOutput (1.7s)
✔ [3386/3393] Built Iut.Foundations.AlgorithmicBridge (2.7s)
✔ [3388/3393] Built Iut.Stage1.CorollarySchema (35s)
✔ [3390/3393] Built Iut.Stage1.SourceObligations (3.5s)
✔ [3391/3397] Built Iut.Stage1.IUTSourceScaffold (2.8s)
✔ [3393/3407] Built Iut.Stage1.IUTStage1Data (3.4s)
⚠ [3410/3425] Built Iut.Stage1.IUTStage1SourceCore (80s)
warning: Iut/Stage1/IUTStage1SourceCore.lean:19880:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.quotient_card_eq_pow_finrank`:
  [FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [FiniteDimensional ℚ_[p] K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20063:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.quotientCosetHaarCharacterEndpoint`:
  [FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [FiniteDimensional ℚ_[p] K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20130:0: automatically included section variable(s) unused in theorem `Iut.Stage1.IUTStage1PadicFiniteExtensionNormedValuedIntegerResidueModuleQuotientCosetHaarCharacterNormalizationSource.unitBallHaarCharacterEndpoint`:
  [FiniteDimensional ℚ_[p] K]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [FiniteDimensional ℚ_[p] K] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20532:4: `rcases hin with ⟨point, hpoint, hpoint_eq⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20533:4: `let preimage : ℤ_[p] := (data.padicIntegerSource.padicIntAddEquivIntegerAddSubgroup).symm ⟨point, hpoint⟩` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20537:4: `have hinteger_eq : (integer : ℚ_[p]) = (p : ℚ_[p]) * (preimage : ℚ_[p]) := by
  simpa [IUTStage1PadicIntegerUnitBallSource.padicIntAddEquivIntegerAddSubgroup, hpreimage_eq] using
    hpoint_eq.symm` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom] at hin` is a flexible tactic modifying `hin`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20530:4: Try this:
  [apply] simp only [RingHom.toAddMonoidHom_eq_coe, AddMonoidHom.mem_ker, AddMonoidHom.coe_coe] at hin
info: Iut/Stage1/IUTStage1SourceCore.lean:20547:4: `change PadicInt.toZMod integer = 0` uses `hin`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20572:4: `refine ⟨(preimage : ℚ_[p]), ?_, ?_⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20573:6: `change (preimage : ℚ_[p]) ∈ data.padicIntegerSource.integerSource.ringOfIntegers` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20576:6: `rw [data.padicIntegerSource.valuedRingOfIntegers_eq_padicIntegerSet]` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20577:6: `exact ⟨preimage, rfl⟩` uses `⊢`!
warning: Iut/Stage1/IUTStage1SourceCore.lean:20570:4: `simp [basePrimeScaledSubgroup,
      IUTStage1PadicFiniteExtensionBasePrimeDilationAddMonoidHom]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: Iut/Stage1/IUTStage1SourceCore.lean:20578:6: `have hpreimage_q : (integer : ℚ_[p]) = ((p : ℤ_[p]) * preimage : ℤ_[p]) := by rw [hpreimage]` uses `⊢`!
✔ [3411/3425] Built Iut.Stage1.IUTStage1Remark312Absorption (13s)
⚠ [3412/3425] Built Iut.Stage1.IUTStage1IUTIVAlgebra (15s)
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5698:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5776:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5822:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5943:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:5991:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1IUTIVAlgebra.lean:6100:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
✔ [3413/3425] Built Iut.Stage1.IUTStage1FiniteLabels (4.5s)
✔ [3414/3425] Built Iut.Stage1.IUTStage1StepX (5.0s)
✔ [3415/3425] Built Iut.Stage1.IUTStage1Gaussian (9.3s)
✔ [3416/3425] Built Iut.Stage1.IUTStage1HodgeSHE (8.9s)
⚠ [3417/3425] Built Iut.Stage1.IUTStage1Theorem311 (23s)
warning: Iut/Stage1/IUTStage1Theorem311.lean:4518:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4523:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4655:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4687:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4692:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4735:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4789:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4824:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4829:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4961:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:4995:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5000:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5138:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5172:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5177:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5320:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5352:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5357:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:5470:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:7525:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:15277:100: This line exceeds the 100 character limit, please shorten it!

Note: This linter can be disabled with `set_option linter.style.longLine false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:15618:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:16875:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:17353:5: unused variable `targetSource`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:18439:5: unused variable `data`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Iut/Stage1/IUTStage1Theorem311.lean:21472:5: unused variable `obligations`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
✖ [3418/3425] Building Iut.Stage1.IUTStage1StepXI (153s)
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/mathlib/.lake/build/lib/lean:/apx/source/.lake/build/lib/lean /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean /apx/source/Iut/Stage1/IUTStage1StepXI.lean -o /apx/source/.lake/build/lib/lean/Iut/Stage1/IUTStage1StepXI.olean -i /apx/source/.lake/build/lib/lean/Iut/Stage1/IUTStage1StepXI.ilean -c /apx/source/.lake/build/ir/Iut/Stage1/IUTStage1StepXI.c --setup /apx/source/.lake/build/ir/Iut/Stage1/IUTStage1StepXI.setup.json --json
error: Lean exited with code 137
Some required targets logged failures:
- Iut.Stage1.IUTStage1StepXI

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

lake build :blueprint

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
error: unknown package facet `blueprint`