My attempts to solve puzzles of Advent of Code
From leanpkg to lake
+2083
-5
+1
-2
2021/AoC.lean
+1
-2
2021/AoC.lean
+66
2021/AoC/Day1.lean
+66
2021/AoC/Day1.lean
···
1
+
namespace Day1
2
+
3
+
open IO.FS
4
+
5
+
section Common
6
+
variable {α β γ ζ : Type u}
7
+
variable {a : Type u -> Type v}
8
+
9
+
def liftA3 [Applicative a] (f: α -> β -> γ -> ζ) (x: a α) (y: a β) (z: a γ) : a ζ := f <$> x <*> y <*> z
10
+
end Common
11
+
12
+
section Part1
13
+
open Prod
14
+
def measureLarge (x: Nat × String) (z: String) : Nat × String :=
15
+
if x.snd.toNat! < z.toNat! then (x.fst + 1, z) else (x.fst, z)
16
+
17
+
def measureLargeNat (x: Nat × Nat) (z: Nat) : Nat × Nat :=
18
+
if x.snd < z then (x.fst + 1, z) else (x.fst, z)
19
+
20
+
def totalIncr (s: Sum Nat String) (xs: Array String := #[]) (ys: Array Nat := #[]): Nat :=
21
+
match s with
22
+
| Sum.inr _ => Prod.fst <| Array.foldl measureLarge (0, Array.get! xs 0) xs
23
+
| _ => Prod.fst <| Array.foldl measureLargeNat (0, Array.get! ys 0) ys
24
+
25
+
end Part1
26
+
27
+
section Part2
28
+
29
+
def lookAheadSum? (xs: Array String) (idx: Nat) : OptionM Nat :=
30
+
let size := xs.size
31
+
if size = 0 then
32
+
Option.none
33
+
else
34
+
let x: OptionM Nat := String.toNat! <$> xs.get? idx
35
+
let y: OptionM Nat := String.toNat! <$> xs.get? (idx + 1)
36
+
let z: OptionM Nat := String.toNat! <$> xs.get? (idx + 2)
37
+
liftA3 (· + · + ·) x y z
38
+
39
+
40
+
def windowEndIndex (length: Nat): Nat := length - (length % 3)
41
+
42
+
/-
43
+
below code might look like imperative shit but Lean is smart enough
44
+
to convert the same via join points. So, everything gets converted
45
+
to functional code in the end
46
+
-/
47
+
def threeWindowSums (xs: Array String): Array Nat := do
48
+
let mut ys := #[]
49
+
for id in [:windowEndIndex xs.size] do
50
+
match (lookAheadSum? xs id) with
51
+
| some x => ys := ys.push x
52
+
| _ => ()
53
+
return ys
54
+
55
+
end Part2
56
+
57
+
def run : IO (Nat × Nat) := do
58
+
let day1 := "./data/day1.txt"
59
+
let readings <- lines day1
60
+
61
+
let part1Total := totalIncr (Sum.inr "") readings
62
+
let part2Total := totalIncr (Sum.inl 0) (ys := threeWindowSums readings)
63
+
64
+
return (part1Total, part2Total)
65
+
66
+
+7
2021/Main.lean
+7
2021/Main.lean
+2000
2021/data/day1.txt
+2000
2021/data/day1.txt
···
1
+
104
2
+
111
3
+
124
4
+
139
5
+
142
6
+
141
7
+
144
8
+
151
9
+
152
10
+
154
11
+
157
12
+
156
13
+
157
14
+
149
15
+
123
16
+
118
17
+
129
18
+
133
19
+
134
20
+
130
21
+
124
22
+
102
23
+
103
24
+
105
25
+
104
26
+
99
27
+
100
28
+
101
29
+
103
30
+
116
31
+
114
32
+
129
33
+
135
34
+
147
35
+
149
36
+
148
37
+
149
38
+
137
39
+
140
40
+
149
41
+
159
42
+
157
43
+
159
44
+
165
45
+
164
46
+
170
47
+
176
48
+
180
49
+
192
50
+
198
51
+
200
52
+
202
53
+
203
54
+
202
55
+
211
56
+
212
57
+
230
58
+
233
59
+
237
60
+
229
61
+
226
62
+
229
63
+
234
64
+
242
65
+
245
66
+
244
67
+
242
68
+
256
69
+
258
70
+
262
71
+
267
72
+
269
73
+
285
74
+
274
75
+
279
76
+
270
77
+
302
78
+
305
79
+
308
80
+
320
81
+
323
82
+
324
83
+
323
84
+
325
85
+
358
86
+
361
87
+
367
88
+
364
89
+
363
90
+
351
91
+
352
92
+
350
93
+
349
94
+
355
95
+
356
96
+
359
97
+
367
98
+
375
99
+
405
100
+
413
101
+
417
102
+
425
103
+
428
104
+
436
105
+
437
106
+
438
107
+
430
108
+
429
109
+
430
110
+
431
111
+
442
112
+
451
113
+
459
114
+
460
115
+
473
116
+
481
117
+
482
118
+
483
119
+
485
120
+
491
121
+
501
122
+
499
123
+
532
124
+
533
125
+
538
126
+
540
127
+
514
128
+
505
129
+
511
130
+
508
131
+
509
132
+
507
133
+
519
134
+
521
135
+
492
136
+
493
137
+
498
138
+
497
139
+
499
140
+
510
141
+
508
142
+
501
143
+
507
144
+
509
145
+
528
146
+
529
147
+
539
148
+
545
149
+
546
150
+
575
151
+
577
152
+
599
153
+
600
154
+
602
155
+
609
156
+
634
157
+
635
158
+
637
159
+
652
160
+
660
161
+
692
162
+
677
163
+
676
164
+
679
165
+
682
166
+
683
167
+
684
168
+
688
169
+
687
170
+
688
171
+
709
172
+
708
173
+
710
174
+
713
175
+
714
176
+
729
177
+
724
178
+
723
179
+
725
180
+
728
181
+
727
182
+
722
183
+
728
184
+
759
185
+
760
186
+
764
187
+
771
188
+
754
189
+
768
190
+
761
191
+
767
192
+
798
193
+
791
194
+
811
195
+
812
196
+
831
197
+
834
198
+
842
199
+
854
200
+
855
201
+
863
202
+
864
203
+
868
204
+
882
205
+
887
206
+
891
207
+
899
208
+
902
209
+
903
210
+
906
211
+
908
212
+
915
213
+
943
214
+
937
215
+
941
216
+
928
217
+
941
218
+
928
219
+
922
220
+
924
221
+
940
222
+
950
223
+
949
224
+
950
225
+
951
226
+
947
227
+
948
228
+
955
229
+
958
230
+
960
231
+
963
232
+
956
233
+
955
234
+
957
235
+
960
236
+
965
237
+
966
238
+
967
239
+
968
240
+
969
241
+
977
242
+
945
243
+
929
244
+
925
245
+
926
246
+
939
247
+
943
248
+
944
249
+
956
250
+
965
251
+
961
252
+
968
253
+
967
254
+
966
255
+
970
256
+
968
257
+
973
258
+
975
259
+
990
260
+
1003
261
+
1005
262
+
1006
263
+
1009
264
+
1011
265
+
1009
266
+
1015
267
+
1016
268
+
1015
269
+
1000
270
+
1005
271
+
1009
272
+
1005
273
+
1011
274
+
1008
275
+
1017
276
+
1016
277
+
1017
278
+
1018
279
+
1013
280
+
1012
281
+
1015
282
+
1012
283
+
1003
284
+
1004
285
+
1005
286
+
1008
287
+
1016
288
+
1021
289
+
1023
290
+
1051
291
+
1052
292
+
1057
293
+
1059
294
+
1067
295
+
1064
296
+
1060
297
+
1062
298
+
1071
299
+
1065
300
+
1077
301
+
1079
302
+
1081
303
+
1085
304
+
1091
305
+
1089
306
+
1092
307
+
1093
308
+
1103
309
+
1083
310
+
1102
311
+
1111
312
+
1113
313
+
1120
314
+
1131
315
+
1132
316
+
1152
317
+
1153
318
+
1162
319
+
1161
320
+
1160
321
+
1145
322
+
1154
323
+
1159
324
+
1148
325
+
1160
326
+
1161
327
+
1162
328
+
1187
329
+
1193
330
+
1184
331
+
1192
332
+
1190
333
+
1191
334
+
1196
335
+
1200
336
+
1205
337
+
1207
338
+
1209
339
+
1208
340
+
1209
341
+
1210
342
+
1211
343
+
1223
344
+
1225
345
+
1226
346
+
1227
347
+
1217
348
+
1211
349
+
1212
350
+
1216
351
+
1209
352
+
1210
353
+
1219
354
+
1218
355
+
1219
356
+
1220
357
+
1219
358
+
1220
359
+
1215
360
+
1242
361
+
1246
362
+
1247
363
+
1233
364
+
1264
365
+
1297
366
+
1284
367
+
1288
368
+
1313
369
+
1333
370
+
1339
371
+
1334
372
+
1341
373
+
1345
374
+
1351
375
+
1350
376
+
1353
377
+
1349
378
+
1352
379
+
1351
380
+
1352
381
+
1353
382
+
1355
383
+
1333
384
+
1334
385
+
1335
386
+
1336
387
+
1337
388
+
1309
389
+
1316
390
+
1315
391
+
1316
392
+
1325
393
+
1343
394
+
1345
395
+
1347
396
+
1334
397
+
1337
398
+
1336
399
+
1337
400
+
1343
401
+
1346
402
+
1347
403
+
1342
404
+
1328
405
+
1326
406
+
1327
407
+
1328
408
+
1320
409
+
1324
410
+
1334
411
+
1336
412
+
1337
413
+
1338
414
+
1348
415
+
1350
416
+
1358
417
+
1374
418
+
1377
419
+
1380
420
+
1366
421
+
1368
422
+
1372
423
+
1376
424
+
1377
425
+
1380
426
+
1382
427
+
1392
428
+
1396
429
+
1402
430
+
1407
431
+
1408
432
+
1423
433
+
1428
434
+
1422
435
+
1424
436
+
1427
437
+
1440
438
+
1439
439
+
1438
440
+
1454
441
+
1460
442
+
1461
443
+
1462
444
+
1466
445
+
1471
446
+
1470
447
+
1448
448
+
1455
449
+
1460
450
+
1470
451
+
1480
452
+
1488
453
+
1497
454
+
1502
455
+
1503
456
+
1505
457
+
1502
458
+
1503
459
+
1510
460
+
1519
461
+
1523
462
+
1526
463
+
1527
464
+
1526
465
+
1530
466
+
1526
467
+
1536
468
+
1534
469
+
1539
470
+
1553
471
+
1557
472
+
1562
473
+
1569
474
+
1570
475
+
1584
476
+
1601
477
+
1564
478
+
1577
479
+
1582
480
+
1584
481
+
1585
482
+
1586
483
+
1589
484
+
1583
485
+
1595
486
+
1608
487
+
1612
488
+
1610
489
+
1605
490
+
1611
491
+
1615
492
+
1619
493
+
1620
494
+
1621
495
+
1624
496
+
1626
497
+
1628
498
+
1621
499
+
1635
500
+
1637
501
+
1645
502
+
1646
503
+
1656
504
+
1658
505
+
1657
506
+
1667
507
+
1672
508
+
1674
509
+
1675
510
+
1678
511
+
1692
512
+
1693
513
+
1696
514
+
1713
515
+
1714
516
+
1715
517
+
1734
518
+
1736
519
+
1738
520
+
1756
521
+
1757
522
+
1780
523
+
1772
524
+
1777
525
+
1776
526
+
1783
527
+
1786
528
+
1792
529
+
1791
530
+
1792
531
+
1797
532
+
1799
533
+
1794
534
+
1811
535
+
1795
536
+
1793
537
+
1780
538
+
1782
539
+
1791
540
+
1789
541
+
1800
542
+
1799
543
+
1797
544
+
1814
545
+
1812
546
+
1818
547
+
1842
548
+
1853
549
+
1871
550
+
1872
551
+
1876
552
+
1877
553
+
1882
554
+
1883
555
+
1874
556
+
1876
557
+
1879
558
+
1893
559
+
1894
560
+
1911
561
+
1877
562
+
1880
563
+
1883
564
+
1884
565
+
1887
566
+
1885
567
+
1892
568
+
1897
569
+
1912
570
+
1917
571
+
1931
572
+
1934
573
+
1935
574
+
1926
575
+
1930
576
+
1945
577
+
1943
578
+
1942
579
+
1943
580
+
1941
581
+
1943
582
+
1947
583
+
1941
584
+
1950
585
+
1955
586
+
1980
587
+
1981
588
+
1986
589
+
1987
590
+
2000
591
+
2005
592
+
1999
593
+
2009
594
+
2010
595
+
2006
596
+
1998
597
+
1999
598
+
2009
599
+
2016
600
+
2017
601
+
1984
602
+
1985
603
+
1986
604
+
1985
605
+
1988
606
+
2011
607
+
2018
608
+
2019
609
+
2023
610
+
2026
611
+
2034
612
+
2041
613
+
2043
614
+
2060
615
+
2068
616
+
2072
617
+
2079
618
+
2082
619
+
2083
620
+
2077
621
+
2109
622
+
2111
623
+
2118
624
+
2146
625
+
2149
626
+
2151
627
+
2148
628
+
2147
629
+
2137
630
+
2138
631
+
2128
632
+
2138
633
+
2139
634
+
2163
635
+
2164
636
+
2194
637
+
2196
638
+
2197
639
+
2198
640
+
2199
641
+
2201
642
+
2211
643
+
2242
644
+
2244
645
+
2248
646
+
2225
647
+
2226
648
+
2235
649
+
2231
650
+
2232
651
+
2233
652
+
2234
653
+
2237
654
+
2233
655
+
2232
656
+
2235
657
+
2217
658
+
2228
659
+
2234
660
+
2235
661
+
2234
662
+
2237
663
+
2238
664
+
2249
665
+
2250
666
+
2252
667
+
2273
668
+
2261
669
+
2278
670
+
2279
671
+
2275
672
+
2274
673
+
2273
674
+
2271
675
+
2284
676
+
2289
677
+
2282
678
+
2284
679
+
2282
680
+
2283
681
+
2286
682
+
2288
683
+
2302
684
+
2321
685
+
2360
686
+
2368
687
+
2369
688
+
2364
689
+
2373
690
+
2379
691
+
2378
692
+
2386
693
+
2391
694
+
2398
695
+
2399
696
+
2400
697
+
2401
698
+
2409
699
+
2416
700
+
2414
701
+
2413
702
+
2412
703
+
2418
704
+
2406
705
+
2429
706
+
2449
707
+
2446
708
+
2449
709
+
2438
710
+
2448
711
+
2450
712
+
2413
713
+
2422
714
+
2424
715
+
2425
716
+
2429
717
+
2430
718
+
2431
719
+
2426
720
+
2428
721
+
2431
722
+
2417
723
+
2419
724
+
2420
725
+
2427
726
+
2421
727
+
2424
728
+
2433
729
+
2434
730
+
2435
731
+
2436
732
+
2462
733
+
2440
734
+
2443
735
+
2442
736
+
2454
737
+
2455
738
+
2458
739
+
2447
740
+
2448
741
+
2450
742
+
2455
743
+
2462
744
+
2464
745
+
2472
746
+
2477
747
+
2482
748
+
2483
749
+
2501
750
+
2511
751
+
2516
752
+
2517
753
+
2514
754
+
2520
755
+
2521
756
+
2525
757
+
2539
758
+
2553
759
+
2554
760
+
2543
761
+
2548
762
+
2544
763
+
2552
764
+
2551
765
+
2553
766
+
2589
767
+
2588
768
+
2594
769
+
2599
770
+
2614
771
+
2615
772
+
2629
773
+
2630
774
+
2639
775
+
2644
776
+
2646
777
+
2665
778
+
2657
779
+
2668
780
+
2669
781
+
2681
782
+
2680
783
+
2684
784
+
2691
785
+
2693
786
+
2686
787
+
2681
788
+
2680
789
+
2683
790
+
2687
791
+
2694
792
+
2696
793
+
2698
794
+
2702
795
+
2690
796
+
2694
797
+
2693
798
+
2698
799
+
2707
800
+
2716
801
+
2714
802
+
2713
803
+
2714
804
+
2724
805
+
2747
806
+
2748
807
+
2750
808
+
2752
809
+
2760
810
+
2756
811
+
2757
812
+
2755
813
+
2756
814
+
2762
815
+
2765
816
+
2778
817
+
2777
818
+
2778
819
+
2777
820
+
2775
821
+
2778
822
+
2770
823
+
2762
824
+
2754
825
+
2755
826
+
2757
827
+
2770
828
+
2771
829
+
2784
830
+
2815
831
+
2836
832
+
2837
833
+
2838
834
+
2839
835
+
2847
836
+
2848
837
+
2850
838
+
2826
839
+
2806
840
+
2820
841
+
2826
842
+
2827
843
+
2832
844
+
2837
845
+
2848
846
+
2859
847
+
2866
848
+
2865
849
+
2873
850
+
2874
851
+
2876
852
+
2879
853
+
2886
854
+
2861
855
+
2865
856
+
2876
857
+
2875
858
+
2872
859
+
2874
860
+
2879
861
+
2889
862
+
2899
863
+
2908
864
+
2909
865
+
2915
866
+
2903
867
+
2915
868
+
2925
869
+
2918
870
+
2919
871
+
2920
872
+
2936
873
+
2932
874
+
2922
875
+
2923
876
+
2935
877
+
2940
878
+
2947
879
+
2969
880
+
2963
881
+
2940
882
+
2944
883
+
2945
884
+
2949
885
+
2964
886
+
2967
887
+
2968
888
+
2985
889
+
2986
890
+
2973
891
+
2974
892
+
2969
893
+
2970
894
+
2965
895
+
2966
896
+
2967
897
+
2953
898
+
2957
899
+
2956
900
+
2964
901
+
2977
902
+
2974
903
+
2983
904
+
2996
905
+
2994
906
+
2992
907
+
2999
908
+
2988
909
+
2974
910
+
2980
911
+
2985
912
+
2986
913
+
2993
914
+
3007
915
+
3008
916
+
3007
917
+
3014
918
+
3013
919
+
3031
920
+
3027
921
+
3029
922
+
3026
923
+
3027
924
+
3035
925
+
3036
926
+
3037
927
+
3052
928
+
3054
929
+
3055
930
+
3059
931
+
3057
932
+
3059
933
+
3058
934
+
3064
935
+
3063
936
+
3065
937
+
3066
938
+
3070
939
+
3072
940
+
3104
941
+
3111
942
+
3103
943
+
3111
944
+
3112
945
+
3138
946
+
3137
947
+
3150
948
+
3137
949
+
3138
950
+
3139
951
+
3142
952
+
3154
953
+
3156
954
+
3157
955
+
3158
956
+
3160
957
+
3152
958
+
3157
959
+
3143
960
+
3147
961
+
3159
962
+
3161
963
+
3162
964
+
3160
965
+
3163
966
+
3164
967
+
3160
968
+
3161
969
+
3167
970
+
3181
971
+
3182
972
+
3190
973
+
3191
974
+
3193
975
+
3192
976
+
3193
977
+
3205
978
+
3206
979
+
3216
980
+
3229
981
+
3230
982
+
3228
983
+
3230
984
+
3218
985
+
3198
986
+
3205
987
+
3233
988
+
3234
989
+
3222
990
+
3217
991
+
3221
992
+
3242
993
+
3243
994
+
3258
995
+
3275
996
+
3276
997
+
3281
998
+
3283
999
+
3304
1000
+
3303
1001
+
3307
1002
+
3309
1003
+
3308
1004
+
3307
1005
+
3304
1006
+
3315
1007
+
3328
1008
+
3355
1009
+
3375
1010
+
3368
1011
+
3374
1012
+
3403
1013
+
3404
1014
+
3406
1015
+
3409
1016
+
3411
1017
+
3409
1018
+
3392
1019
+
3400
1020
+
3404
1021
+
3405
1022
+
3406
1023
+
3403
1024
+
3405
1025
+
3408
1026
+
3430
1027
+
3439
1028
+
3440
1029
+
3458
1030
+
3461
1031
+
3469
1032
+
3484
1033
+
3490
1034
+
3491
1035
+
3492
1036
+
3506
1037
+
3511
1038
+
3513
1039
+
3524
1040
+
3525
1041
+
3534
1042
+
3535
1043
+
3491
1044
+
3493
1045
+
3509
1046
+
3538
1047
+
3540
1048
+
3545
1049
+
3544
1050
+
3543
1051
+
3552
1052
+
3554
1053
+
3559
1054
+
3565
1055
+
3567
1056
+
3576
1057
+
3580
1058
+
3581
1059
+
3589
1060
+
3594
1061
+
3607
1062
+
3615
1063
+
3618
1064
+
3638
1065
+
3657
1066
+
3665
1067
+
3664
1068
+
3665
1069
+
3658
1070
+
3665
1071
+
3667
1072
+
3668
1073
+
3682
1074
+
3684
1075
+
3687
1076
+
3699
1077
+
3712
1078
+
3716
1079
+
3720
1080
+
3728
1081
+
3744
1082
+
3742
1083
+
3740
1084
+
3752
1085
+
3763
1086
+
3760
1087
+
3757
1088
+
3760
1089
+
3762
1090
+
3767
1091
+
3758
1092
+
3738
1093
+
3739
1094
+
3737
1095
+
3738
1096
+
3762
1097
+
3767
1098
+
3792
1099
+
3820
1100
+
3821
1101
+
3822
1102
+
3824
1103
+
3825
1104
+
3829
1105
+
3821
1106
+
3794
1107
+
3800
1108
+
3799
1109
+
3801
1110
+
3800
1111
+
3820
1112
+
3835
1113
+
3836
1114
+
3856
1115
+
3859
1116
+
3867
1117
+
3871
1118
+
3888
1119
+
3889
1120
+
3893
1121
+
3898
1122
+
3897
1123
+
3894
1124
+
3921
1125
+
3917
1126
+
3916
1127
+
3917
1128
+
3925
1129
+
3922
1130
+
3923
1131
+
3930
1132
+
3931
1133
+
3932
1134
+
3935
1135
+
3936
1136
+
3948
1137
+
3947
1138
+
3948
1139
+
3961
1140
+
3968
1141
+
3998
1142
+
3999
1143
+
4000
1144
+
4001
1145
+
3994
1146
+
3977
1147
+
3979
1148
+
3980
1149
+
3976
1150
+
3982
1151
+
3988
1152
+
3992
1153
+
4000
1154
+
4001
1155
+
4007
1156
+
4008
1157
+
4004
1158
+
4038
1159
+
4025
1160
+
4005
1161
+
3986
1162
+
3987
1163
+
3989
1164
+
3991
1165
+
3983
1166
+
3982
1167
+
4004
1168
+
4005
1169
+
4012
1170
+
4040
1171
+
4060
1172
+
4070
1173
+
4064
1174
+
4086
1175
+
4096
1176
+
4100
1177
+
4109
1178
+
4117
1179
+
4125
1180
+
4142
1181
+
4148
1182
+
4149
1183
+
4154
1184
+
4153
1185
+
4161
1186
+
4162
1187
+
4155
1188
+
4157
1189
+
4159
1190
+
4161
1191
+
4186
1192
+
4202
1193
+
4201
1194
+
4202
1195
+
4201
1196
+
4207
1197
+
4209
1198
+
4212
1199
+
4214
1200
+
4211
1201
+
4212
1202
+
4232
1203
+
4233
1204
+
4239
1205
+
4250
1206
+
4243
1207
+
4242
1208
+
4246
1209
+
4247
1210
+
4246
1211
+
4245
1212
+
4244
1213
+
4251
1214
+
4255
1215
+
4259
1216
+
4261
1217
+
4262
1218
+
4270
1219
+
4252
1220
+
4267
1221
+
4271
1222
+
4272
1223
+
4275
1224
+
4277
1225
+
4276
1226
+
4277
1227
+
4261
1228
+
4275
1229
+
4278
1230
+
4283
1231
+
4304
1232
+
4314
1233
+
4316
1234
+
4323
1235
+
4325
1236
+
4324
1237
+
4331
1238
+
4342
1239
+
4348
1240
+
4352
1241
+
4353
1242
+
4362
1243
+
4389
1244
+
4387
1245
+
4362
1246
+
4360
1247
+
4373
1248
+
4392
1249
+
4393
1250
+
4397
1251
+
4399
1252
+
4400
1253
+
4405
1254
+
4410
1255
+
4405
1256
+
4406
1257
+
4414
1258
+
4403
1259
+
4410
1260
+
4413
1261
+
4417
1262
+
4440
1263
+
4441
1264
+
4442
1265
+
4443
1266
+
4446
1267
+
4459
1268
+
4468
1269
+
4467
1270
+
4475
1271
+
4474
1272
+
4467
1273
+
4473
1274
+
4474
1275
+
4473
1276
+
4472
1277
+
4480
1278
+
4467
1279
+
4468
1280
+
4475
1281
+
4477
1282
+
4478
1283
+
4479
1284
+
4492
1285
+
4493
1286
+
4501
1287
+
4504
1288
+
4503
1289
+
4510
1290
+
4476
1291
+
4482
1292
+
4484
1293
+
4485
1294
+
4486
1295
+
4497
1296
+
4505
1297
+
4512
1298
+
4518
1299
+
4519
1300
+
4521
1301
+
4524
1302
+
4526
1303
+
4533
1304
+
4555
1305
+
4558
1306
+
4573
1307
+
4575
1308
+
4576
1309
+
4564
1310
+
4559
1311
+
4562
1312
+
4573
1313
+
4572
1314
+
4577
1315
+
4580
1316
+
4568
1317
+
4569
1318
+
4570
1319
+
4576
1320
+
4577
1321
+
4578
1322
+
4568
1323
+
4575
1324
+
4582
1325
+
4589
1326
+
4586
1327
+
4599
1328
+
4603
1329
+
4587
1330
+
4618
1331
+
4600
1332
+
4599
1333
+
4598
1334
+
4607
1335
+
4596
1336
+
4608
1337
+
4610
1338
+
4622
1339
+
4626
1340
+
4650
1341
+
4664
1342
+
4679
1343
+
4675
1344
+
4687
1345
+
4685
1346
+
4684
1347
+
4685
1348
+
4680
1349
+
4706
1350
+
4704
1351
+
4693
1352
+
4705
1353
+
4712
1354
+
4713
1355
+
4712
1356
+
4718
1357
+
4728
1358
+
4733
1359
+
4735
1360
+
4759
1361
+
4758
1362
+
4763
1363
+
4764
1364
+
4766
1365
+
4767
1366
+
4793
1367
+
4794
1368
+
4795
1369
+
4796
1370
+
4791
1371
+
4780
1372
+
4761
1373
+
4768
1374
+
4771
1375
+
4777
1376
+
4778
1377
+
4789
1378
+
4788
1379
+
4789
1380
+
4795
1381
+
4802
1382
+
4791
1383
+
4789
1384
+
4790
1385
+
4789
1386
+
4801
1387
+
4809
1388
+
4812
1389
+
4806
1390
+
4826
1391
+
4835
1392
+
4838
1393
+
4840
1394
+
4846
1395
+
4853
1396
+
4856
1397
+
4858
1398
+
4859
1399
+
4864
1400
+
4862
1401
+
4865
1402
+
4867
1403
+
4868
1404
+
4872
1405
+
4875
1406
+
4866
1407
+
4859
1408
+
4860
1409
+
4857
1410
+
4866
1411
+
4872
1412
+
4873
1413
+
4872
1414
+
4884
1415
+
4887
1416
+
4885
1417
+
4895
1418
+
4898
1419
+
4902
1420
+
4901
1421
+
4902
1422
+
4898
1423
+
4887
1424
+
4886
1425
+
4901
1426
+
4913
1427
+
4914
1428
+
4915
1429
+
4918
1430
+
4920
1431
+
4918
1432
+
4959
1433
+
4958
1434
+
4953
1435
+
4982
1436
+
4987
1437
+
4972
1438
+
4988
1439
+
4999
1440
+
4996
1441
+
4997
1442
+
5022
1443
+
5040
1444
+
5038
1445
+
5037
1446
+
5059
1447
+
5062
1448
+
5096
1449
+
5097
1450
+
5102
1451
+
5127
1452
+
5138
1453
+
5176
1454
+
5175
1455
+
5179
1456
+
5180
1457
+
5181
1458
+
5180
1459
+
5213
1460
+
5216
1461
+
5215
1462
+
5214
1463
+
5219
1464
+
5222
1465
+
5225
1466
+
5227
1467
+
5249
1468
+
5286
1469
+
5287
1470
+
5288
1471
+
5302
1472
+
5306
1473
+
5307
1474
+
5316
1475
+
5326
1476
+
5328
1477
+
5327
1478
+
5326
1479
+
5327
1480
+
5305
1481
+
5309
1482
+
5310
1483
+
5305
1484
+
5318
1485
+
5319
1486
+
5322
1487
+
5323
1488
+
5333
1489
+
5355
1490
+
5359
1491
+
5369
1492
+
5368
1493
+
5359
1494
+
5384
1495
+
5387
1496
+
5420
1497
+
5442
1498
+
5453
1499
+
5455
1500
+
5454
1501
+
5446
1502
+
5445
1503
+
5448
1504
+
5455
1505
+
5474
1506
+
5472
1507
+
5478
1508
+
5482
1509
+
5483
1510
+
5490
1511
+
5523
1512
+
5534
1513
+
5535
1514
+
5536
1515
+
5535
1516
+
5537
1517
+
5538
1518
+
5544
1519
+
5547
1520
+
5539
1521
+
5540
1522
+
5558
1523
+
5559
1524
+
5573
1525
+
5574
1526
+
5578
1527
+
5576
1528
+
5584
1529
+
5610
1530
+
5618
1531
+
5609
1532
+
5600
1533
+
5602
1534
+
5627
1535
+
5637
1536
+
5607
1537
+
5603
1538
+
5612
1539
+
5608
1540
+
5611
1541
+
5622
1542
+
5623
1543
+
5625
1544
+
5626
1545
+
5628
1546
+
5634
1547
+
5646
1548
+
5655
1549
+
5658
1550
+
5667
1551
+
5678
1552
+
5682
1553
+
5685
1554
+
5708
1555
+
5712
1556
+
5711
1557
+
5718
1558
+
5716
1559
+
5719
1560
+
5720
1561
+
5722
1562
+
5753
1563
+
5757
1564
+
5752
1565
+
5753
1566
+
5768
1567
+
5774
1568
+
5750
1569
+
5730
1570
+
5728
1571
+
5733
1572
+
5734
1573
+
5729
1574
+
5743
1575
+
5744
1576
+
5746
1577
+
5748
1578
+
5757
1579
+
5771
1580
+
5779
1581
+
5759
1582
+
5763
1583
+
5783
1584
+
5796
1585
+
5797
1586
+
5799
1587
+
5815
1588
+
5816
1589
+
5817
1590
+
5831
1591
+
5838
1592
+
5834
1593
+
5840
1594
+
5846
1595
+
5852
1596
+
5850
1597
+
5858
1598
+
5861
1599
+
5864
1600
+
5867
1601
+
5870
1602
+
5879
1603
+
5903
1604
+
5904
1605
+
5930
1606
+
5931
1607
+
5936
1608
+
5939
1609
+
5941
1610
+
5943
1611
+
5936
1612
+
5938
1613
+
5943
1614
+
5951
1615
+
5962
1616
+
5955
1617
+
5950
1618
+
5945
1619
+
5946
1620
+
5951
1621
+
5950
1622
+
5951
1623
+
5950
1624
+
5956
1625
+
5957
1626
+
5959
1627
+
5975
1628
+
5977
1629
+
5992
1630
+
5994
1631
+
5997
1632
+
5999
1633
+
6011
1634
+
6012
1635
+
6013
1636
+
6014
1637
+
6013
1638
+
6028
1639
+
6032
1640
+
6058
1641
+
6064
1642
+
6065
1643
+
6078
1644
+
6079
1645
+
6080
1646
+
6086
1647
+
6089
1648
+
6091
1649
+
6077
1650
+
6083
1651
+
6051
1652
+
6044
1653
+
6058
1654
+
6062
1655
+
6069
1656
+
6050
1657
+
6048
1658
+
6058
1659
+
6086
1660
+
6093
1661
+
6094
1662
+
6106
1663
+
6107
1664
+
6115
1665
+
6114
1666
+
6115
1667
+
6112
1668
+
6117
1669
+
6131
1670
+
6130
1671
+
6132
1672
+
6140
1673
+
6164
1674
+
6167
1675
+
6163
1676
+
6177
1677
+
6180
1678
+
6181
1679
+
6183
1680
+
6184
1681
+
6186
1682
+
6193
1683
+
6196
1684
+
6197
1685
+
6200
1686
+
6201
1687
+
6198
1688
+
6202
1689
+
6203
1690
+
6193
1691
+
6211
1692
+
6227
1693
+
6222
1694
+
6223
1695
+
6222
1696
+
6224
1697
+
6207
1698
+
6197
1699
+
6198
1700
+
6196
1701
+
6204
1702
+
6206
1703
+
6207
1704
+
6210
1705
+
6209
1706
+
6210
1707
+
6209
1708
+
6229
1709
+
6232
1710
+
6233
1711
+
6235
1712
+
6237
1713
+
6232
1714
+
6254
1715
+
6268
1716
+
6275
1717
+
6290
1718
+
6292
1719
+
6300
1720
+
6301
1721
+
6295
1722
+
6297
1723
+
6298
1724
+
6301
1725
+
6308
1726
+
6317
1727
+
6318
1728
+
6326
1729
+
6319
1730
+
6320
1731
+
6319
1732
+
6321
1733
+
6329
1734
+
6332
1735
+
6331
1736
+
6342
1737
+
6348
1738
+
6369
1739
+
6370
1740
+
6390
1741
+
6420
1742
+
6423
1743
+
6436
1744
+
6437
1745
+
6452
1746
+
6444
1747
+
6445
1748
+
6456
1749
+
6457
1750
+
6444
1751
+
6448
1752
+
6457
1753
+
6489
1754
+
6491
1755
+
6502
1756
+
6507
1757
+
6510
1758
+
6495
1759
+
6497
1760
+
6505
1761
+
6507
1762
+
6511
1763
+
6513
1764
+
6516
1765
+
6520
1766
+
6523
1767
+
6532
1768
+
6534
1769
+
6535
1770
+
6548
1771
+
6561
1772
+
6560
1773
+
6566
1774
+
6567
1775
+
6586
1776
+
6589
1777
+
6592
1778
+
6598
1779
+
6602
1780
+
6603
1781
+
6621
1782
+
6630
1783
+
6632
1784
+
6634
1785
+
6660
1786
+
6661
1787
+
6662
1788
+
6642
1789
+
6657
1790
+
6659
1791
+
6655
1792
+
6658
1793
+
6661
1794
+
6662
1795
+
6663
1796
+
6672
1797
+
6661
1798
+
6664
1799
+
6665
1800
+
6678
1801
+
6682
1802
+
6683
1803
+
6669
1804
+
6663
1805
+
6658
1806
+
6663
1807
+
6680
1808
+
6685
1809
+
6686
1810
+
6687
1811
+
6693
1812
+
6687
1813
+
6680
1814
+
6686
1815
+
6694
1816
+
6676
1817
+
6675
1818
+
6695
1819
+
6698
1820
+
6716
1821
+
6717
1822
+
6720
1823
+
6728
1824
+
6734
1825
+
6735
1826
+
6733
1827
+
6743
1828
+
6745
1829
+
6758
1830
+
6757
1831
+
6763
1832
+
6762
1833
+
6761
1834
+
6790
1835
+
6793
1836
+
6798
1837
+
6799
1838
+
6807
1839
+
6808
1840
+
6822
1841
+
6828
1842
+
6795
1843
+
6793
1844
+
6795
1845
+
6790
1846
+
6791
1847
+
6794
1848
+
6799
1849
+
6808
1850
+
6815
1851
+
6827
1852
+
6856
1853
+
6857
1854
+
6882
1855
+
6883
1856
+
6885
1857
+
6886
1858
+
6903
1859
+
6902
1860
+
6903
1861
+
6904
1862
+
6892
1863
+
6893
1864
+
6912
1865
+
6893
1866
+
6888
1867
+
6887
1868
+
6891
1869
+
6892
1870
+
6891
1871
+
6898
1872
+
6899
1873
+
6900
1874
+
6901
1875
+
6900
1876
+
6901
1877
+
6913
1878
+
6914
1879
+
6918
1880
+
6932
1881
+
6944
1882
+
6945
1883
+
6960
1884
+
6963
1885
+
6961
1886
+
6966
1887
+
6968
1888
+
6974
1889
+
6979
1890
+
6980
1891
+
6981
1892
+
6982
1893
+
7003
1894
+
7023
1895
+
7034
1896
+
7035
1897
+
7068
1898
+
7087
1899
+
7088
1900
+
7089
1901
+
7098
1902
+
7104
1903
+
7093
1904
+
7095
1905
+
7102
1906
+
7129
1907
+
7120
1908
+
7123
1909
+
7153
1910
+
7155
1911
+
7157
1912
+
7158
1913
+
7157
1914
+
7151
1915
+
7167
1916
+
7190
1917
+
7208
1918
+
7197
1919
+
7200
1920
+
7201
1921
+
7224
1922
+
7223
1923
+
7217
1924
+
7224
1925
+
7225
1926
+
7227
1927
+
7228
1928
+
7233
1929
+
7234
1930
+
7265
1931
+
7266
1932
+
7267
1933
+
7286
1934
+
7296
1935
+
7297
1936
+
7299
1937
+
7295
1938
+
7296
1939
+
7297
1940
+
7283
1941
+
7259
1942
+
7255
1943
+
7259
1944
+
7260
1945
+
7267
1946
+
7275
1947
+
7273
1948
+
7274
1949
+
7277
1950
+
7276
1951
+
7289
1952
+
7291
1953
+
7297
1954
+
7298
1955
+
7299
1956
+
7298
1957
+
7300
1958
+
7307
1959
+
7308
1960
+
7312
1961
+
7332
1962
+
7341
1963
+
7342
1964
+
7335
1965
+
7348
1966
+
7349
1967
+
7345
1968
+
7344
1969
+
7345
1970
+
7358
1971
+
7357
1972
+
7359
1973
+
7397
1974
+
7398
1975
+
7401
1976
+
7406
1977
+
7425
1978
+
7424
1979
+
7429
1980
+
7430
1981
+
7433
1982
+
7435
1983
+
7436
1984
+
7437
1985
+
7430
1986
+
7429
1987
+
7439
1988
+
7440
1989
+
7454
1990
+
7456
1991
+
7438
1992
+
7439
1993
+
7421
1994
+
7439
1995
+
7438
1996
+
7441
1997
+
7421
1998
+
7422
1999
+
7424
2000
+
7440
+6
2021/lakefile.lean
+6
2021/lakefile.lean
+1
2021/lean-toolchain
+1
2021/lean-toolchain
···
1
+
leanprover/lean4:nightly-2021-12-04