1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85
86. 86
87. 87
88. 88
89. 89
90. 90
91. 91
92. 92
93. 93
94. 94
95. 95
96. 96
97. 97
98. 98
99. 99
100. 100
101. 101
102. 102
103. 103
104. 104
105. 105
106. 106
107. 107
108. 108
109. 109
110. 110
111. 111
112. 112
113. 113
114. 114
115. 115
116. 116
117. 117
118. 118
119. 119
120. 120
121. 121
122. 122
123. 123
124. 124
125. 125
126. 126
127. 127
128. 128
129. 129
130. 130
131. 131
132. 132
133. 133
134. 134
135. 135
136. 136
137. 137
138. 138
139. 139
140. 140
141. 141
142. 142
143. 143
144. 144
145. 145
146. 146
147. 147
148. 148
149. 149
150. 150
151. 151
152. 152
153. 153
154. 154
155. 155
156. 156
157. 157
158. 158
159. 159
160. 160
161. 161
162. 162
163. 163
164. 164
165. 165
166. 166
167. 167
168. 168
169. 169
170. 170
171. 171
172. 172
173. 173
174. 174
175. 175
176. 176
177. 177
178. 178
179. 179
180. 180
181. 181
182. 182
183. 183
184. 184
185. 185
186. 186
187. 187
188. 188
189. 189
190. 190
191. 191
192. 192
193. 193
194. 194
195. 195
196. 196
197. 197
198. 198
199. 199
200. 200
201. 201
202. 202
203. 203
204. 204
205. 205
206. 206
207. 207
208. 208
209. 209
210. 210
211. 211
212. 212
213. 213
214. 214
215. 215
216. 216
217. 217
218. 218
219. 219
220. 220
221. 221
222. 222
223. 223
224. 224
225. 225
226. 226
227. 227
228. 228
229. 229
230. 230
231. 231
232. 232
233. 233
234. 234
235. 235
236. 236
237. 237
238. 238
239. 239
240. 240
241. 241
242. 242
243. 243
244. 244
245. 245
246. 246
247. 247
248. 248
249. 249
250. 250
251. 251
252. 252
253. 253
254. 254
255. 255
256. 256
257. 257
258. 258
259. 259
260. 260
261. 261
262. 262
263. 263
264. 264
265. 265
266. 266
267. 267
268. 268
269. 269
270. 270
271. 271
272. 272
273. 273
274. 274
275. 275
276. 276
277. 277
278. 278
279. 279
280. 280
281. 281
282. 282
283. 283
284. 284
285. 285
286. 286
287. 287
288. 288
289. 289
290. 290
291. 291
292. 292
293. 293
294. 294
295. 295
296. 296
297. 297
298. 298
299. 299
300. 300
301. 301
302. 302
303. 303
304. 304
305. 305
306. 306
307. 307
308. 308
309. 309
310. 310
311. 311
312. 312
313. 313
314. 314
315. 315
316. 316
317. 317
318. 318
319. 319
320. 320
321. 321
322. 322
323. 323
324. 324
325. 325
326. 326
327. 327
328. 328
329. 329
330. 330
331. 331
332. 332
333. 333
334. 334
335. 335
336. 336
337. 337
338. 338
339. 339
340. 340
341. 341
342. 342
343. 343
344. 344
345. 345
346. 346
347. 347
348. 348
349. 349
350. 350
351. 351
352. 352
353. 353
354. 354
355. 355
356. 356
357. 357
358. 358
359. 359
360. 360
361. 361
362. 362
363. 363
364. 364
365. 365
366. 366
367. 367
368. 368
369. 369
370. 370
371. 371
372. 372
373. 373
374. 374
375. 375
376. 376
377. 377
378. 378
379. 379
380. 380
381. 381
382. 382
383. 383
384. 384
385. 385
386. 386
387. 387
388. 388
389. 389
390. 390
391. 391
392. 392
393. 393
394. 394
395. 395
396. 396
397. 397
398. 398
399. 399
400. 400
401. 401
402. 402
403. 403
404. 404
405. 405
406. 406
407. 407
408. 408
409. 409
410. 410
411. 411
412. 412
413. 413
414. 414
415. 415
416. 416
417. 417
418. 418
419. 419
420. 420
421. 421
422. 422
423. 423
424. 424
425. 425
426. 426
427. 427
428. 428
429. 429
430. 430
431. 431
432. 432
433. 433
434. 434
435. 435
436. 436
437. 437
438. 438
439. 439
440. 440
441. 441
442. 442
443. 443
444. 444
445. 445
446. 446
447. 447
448. 448
449. 449
450. 450
451. 451
452. 452
453. 453
454. 454
455. 455
456. 456
457. 457
458. 458
459. 459
460. 460
461. 461
462. 462
463. 463
464. 464
465. 465
466. 466
467. 467
468. 468
469. 469
470. 470
471. 471
472. 472
473. 473
474. 474
475. 475
476. 476
477. 477
478. 478
479. 479
480. 480
481. 481
482. 482
483. 483
484. 484
485. 485
486. 486
487. 487
488. 488
489. 489
490. 490
491. 491
492. 492
493. 493
494. 494
495. 495
496. 496
497. 497
498. 498
499. 499
500. 500
501. 501
502. 502
503. 503
504. 504
505. 505
506. 506
507. 507
508. 508
509. 509
510. 510
511. 511
512. 512
513. 513
514. 514
515. 515
516. 516
517. 517
518. 518
519. 519
520. 520
521. 521
522. 522
523. 523
524. 524
525. 525
526. 526
527. 527
528. 528
529. 529
530. 530
531. 531
532. 532
533. 533
534. 534
535. 535
536. 536
537. 537
538. 538
539. 539
540. 540
541. 541
542. 542
543. 543
544. 544
545. 545
546. 546
547. 547
548. 548
549. 549
550. 550
551. 551
552. 552
553. 553
554. 554
555. 555
556. 556
557. 557
558. 558
559. 559
560. 560
561. 561
562. 562
563. 563
564. 564
565. 565
566. 566
567. 567
568. 568
569. 569
570. 570
571. 571
572. 572
573. 573
574. 574
575. 575
576. 576
577. 577
578. 578
579. 579
580. 580
581. 581
582. 582
583. 583
584. 584
585. 585
586. 586
587. 587
588. 588
589. 589
590. 590
591. 591
592. 592
593. 593
594. 594
595. 595
596. 596
597. 597
598. 598
599. 599
600. 600
601. 601
602. 602
603. 603
604. 604
605. 605
606. 606
607. 607
608. 608
609. 609
610. 610
611. 611
612. 612
613. 613
614. 614
615. 615
616. 616
617. 617
618. 618
619. 619
620. 620
621. 621
622. 622
623. 623
624. 624
625. 625
626. 626
627. 627
628. 628
629. 629
630. 630
631. 631
632. 632
633. 633
634. 634
635. 635
636. 636
637. 637
638. 638
639. 639
640. 640
641. 641
642. 642
643. 643
644. 644
645. 645
646. 646
647. 647
648. 648
649. 649
650. 650
651. 651
652. 652
653. 653
654. 654
655. 655
656. 656
657. 657
658. 658
659. 659
660. 660
661. 661
662. 662
663. 663
664. 664
665. 665
666. 666
667. 667
668. 668
669. 669
670. 670
671. 671
672. 672
673. 673
674. 674
675. 675
676. 676
677. 677
678. 678
679. 679
680. 680
681. 681
682. 682
683. 683
684. 684
685. 685
686. 686
687. 687
688. 688
689. 689
690. 690
691. 691
692. 692
693. 693
694. 694
695. 695
696. 696
697. 697
698. 698
699. 699
700. 700
701. 701
702. 702
703. 703
704. 704
705. 705
706. 706
707. 707
708. 708
709. 709
710. 710
711. 711
712. 712
713. 713
714. 714
715. 715
716. 716
717. 717
718. 718
719. 719
720. 720
721. 721
722. 722
723. 723
724. 724
725. 725
726. 726
727. 727
728. 728
729. 729
730. 730
731. 731
732. 732
733. 733
734. 734
735. 735
736. 736
737. 737
738. 738
739. 739
740. 740
741. 741
742. 742
743. 743
744. 744
745. 745
746. 746
747. 747
748. 748
749. 749
750. 750
751. 751
752. 752
753. 753
754. 754
755. 755
756. 756
757. 757
758. 758
759. 759
760. 760
761. 761
762. 762
763. 763
764. 764
765. 765
766. 766
767. 767
768. 768
769. 769
770. 770
771. 771
772. 772
773. 773
774. 774
775. 775
776. 776
777. 777
778. 778
779. 779
780. 780
781. 781
782. 782
783. 783
784. 784
785. 785
786. 786
787. 787
788. 788
789. 789
790. 790
791. 791
792. 792
793. 793
794. 794
795. 795
796. 796
797. 797
798. 798
799. 799
800. 800
801. 801
802. 802
803. 803
804. 804
805. 805
806. 806
807. 807
808. 808
809. 809
810. 810
811. 811
812. 812
813. 813
814. 814
815. 815
816. 816
817. 817
818. 818
819. 819
820. 820
821. 821
822. 822
823. 823
824. 824
825. 825
826. 826
827. 827
828. 828
829. 829
830. 830
831. 831
832. 832
833. 833
834. 834
835. 835
836. 836
837. 837
838. 838
839. 839
840. 840
841. 841
842. 842
843. 843
844. 844
845. 845
846. 846
847. 847
848. 848
849. 849
850. 850
851. 851
852. 852
853. 853
854. 854
855. 855
856. 856
857. 857
858. 858
859. 859
860. 860
861. 861
862. 862
863. 863
864. 864
865. 865
866. 866
867. 867
868. 868
869. 869
870. 870
871. 871
872. 872
873. 873
874. 874
875. 875
876. 876
877. 877
878. 878
879. 879
880. 880
881. 881
882. 882
883. 883
884. 884
885. 885
886. 886
887. 887
888. 888
889. 889
890. 890
891. 891
892. 892
893. 893
894. 894
895. 895
896. 896
897. 897
898. 898
899. 899
900. 900
901. 901
902. 902
903. 903
904. 904
905. 905
906. 906
907. 907
908. 908
909. 909
910. 910
911. 911
912. 912
913. 913
914. 914
915. 915
916. 916
917. 917
918. 918
919. 919
920. 920
921. 921
922. 922
923. 923
924. 924
925. 925
926. 926
927. 927
928. 928
929. 929
930. 930
931. 931
932. 932
933. 933
934. 934
935. 935
936. 936
937. 937
938. 938
939. 939
940. 940
941. 941
942. 942
943. 943
944. 944
945. 945
946. 946
947. 947
948. 948
949. 949
950. 950
951. 951
952. 952
953. 953
954. 954
955. 955
956. 956
957. 957
958. 958
959. 959
960. 960
961. 961
962. 962
963. 963
964. 964
965. 965
966. 966
967. 967
968. 968
969. 969
970. 970
971. 971
972. 972
973. 973
974. 974
975. 975
976. 976
977. 977
978. 978
979. 979
980. 980
981. 981
982. 982
983. 983
984. 984
985. 985
986. 986
987. 987
988. 988
989. 989
990. 990
991. 991
992. 992
993. 993
994. 994
995. 995
996. 996
997. 997
998. 998
999. 999
1000. 1000
1001. 1001
1002. 1002
1003. 1003
1004. 1004
1005. 1005
1006. 1006
1007. 1007
1008. 1008
1009. 1009
1010. 1010
1011. 1011
1012. 1012
1013. 1013
1014. 1014
1015. 1015
1016. 1016
1017. 1017
1018. 1018
1019. 1019
1020. 1020
1021. 1021
1022. 1022
1023. 1023
1024. 1024
1025. 1025
1026. 1026
1027. 1027
1028. 1028
1029. 1029
1030. 1030
1031. 1031
1032. 1032
1033. 1033
1034. 1034
1035. 1035
1036. 1036
1037. 1037
1038. 1038
1039. 1039
1040. 1040
1041. 1041
1042. 1042
1043. 1043
1044. 1044
1045. 1045
1046. 1046
1047. 1047
1048. 1048
1049. 1049
1050. 1050
1051. 1051
1052. 1052
1053. 1053
1054. 1054
1055. 1055
1056. 1056
1057. 1057
1058. 1058
1059. 1059
1060. 1060
1061. 1061
1062. 1062
1063. 1063
1064. 1064
1065. 1065
1066. 1066
1067. 1067
1068. 1068
1069. 1069
1070. 1070
1071. 1071
1072. 1072
1073. 1073
1074. 1074
1075. 1075
1076. 1076
1077. 1077
1078. 1078
1079. 1079
1080. 1080
1081. 1081
1082. 1082
1083. 1083
1084. 1084
1085. 1085
1086. 1086
1087. 1087
1088. 1088
1089. 1089
1090. 1090
1091. 1091
1092. 1092
1093. 1093
1094. 1094
1095. 1095
1096. 1096
1097. 1097
1098. 1098
1099. 1099
1100. 1100
1101. 1101
1102. 1102
1103. 1103
1104. 1104
1105. 1105
1106. 1106
1107. 1107
1108. 1108
1109. 1109
1110. 1110
1111. 1111
1112. 1112
1113. 1113
1114. 1114
1115. 1115
1116. 1116
1117. 1117
1118. 1118
1119. 1119
1120. 1120
1121. 1121
1122. 1122
1123. 1123
1124. 1124
1125. 1125
1126. 1126
1127. 1127
1128. 1128
1129. 1129
1130. 1130
1131. 1131
1132. 1132
1133. 1133
1134. 1134
1135. 1135
1136. 1136
1137. 1137
1138. 1138
1139. 1139
1140. 1140
1141. 1141
1142. 1142
1143. 1143
1144. 1144
1145. 1145
1146. 1146
1147. 1147
1148. 1148
1149. 1149
1150. 1150
1151. 1151
1152. 1152
1153. 1153
1154. 1154
1155. 1155
1156. 1156
1157. 1157
1158. 1158
1159. 1159
1160. 1160
1161. 1161
1162. 1162
1163. 1163
1164. 1164
1165. 1165
1166. 1166
1167. 1167
1168. 1168
1169. 1169
1170. 1170
1171. 1171
1172. 1172
1173. 1173
1174. 1174
1175. 1175
1176. 1176
1177. 1177
1178. 1178

<!DOCTYPE html>
<html class="writer-html5" lang="en" data-content_root="./">
<head>
  <meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>5. Elementary Number Theory &mdash; Mathematics in Lean 0.1 documentation</title>
      <link rel="stylesheet" type="text/css" href="_static/pygments.css?v=80d5e7a1" />
      <link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=e59714d7" />
      <link rel="stylesheet" type="text/css" href="_static/css/custom.css?v=0731ccc3" />

  
    <link rel="shortcut icon" href="_static/favicon.ico"/>
      <script src="_static/jquery.js?v=5d32c60e"></script>
      <script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
      <script src="_static/documentation_options.js?v=2709fde1"></script>
      <script src="_static/doctools.js?v=9bcbadda"></script>
      <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
      <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="6. Structures" href="C06_Structures.html" />
    <link rel="prev" title="4. Sets and Functions" href="C04_Sets_and_Functions.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >

          
          
          <a href="index.html" class="icon icon-home">
            Mathematics in Lean
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul class="current">
<li class="toctree-l1"><a class="reference internal" href="C01_Introduction.html">1. Introduction</a></li>
<li class="toctree-l1"><a class="reference internal" href="C02_Basics.html">2. Basics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C03_Logic.html">3. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="C04_Sets_and_Functions.html">4. Sets and Functions</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">5. Elementary Number Theory</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#irrational-roots">5.1. Irrational Roots</a></li>
<li class="toctree-l2"><a class="reference internal" href="#induction-and-recursion">5.2. Induction and Recursion</a></li>
<li class="toctree-l2"><a class="reference internal" href="#infinitely-many-primes">5.3. Infinitely Many Primes</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C06_Structures.html">6. Structures</a></li>
<li class="toctree-l1"><a class="reference internal" href="C07_Hierarchies.html">7. Hierarchies</a></li>
<li class="toctree-l1"><a class="reference internal" href="C08_Groups_and_Rings.html">8. Groups and Rings</a></li>
<li class="toctree-l1"><a class="reference internal" href="C09_Linear_Algebra.html">9. Linear algebra</a></li>
<li class="toctree-l1"><a class="reference internal" href="C10_Topology.html">10. Topology</a></li>
<li class="toctree-l1"><a class="reference internal" href="C11_Differential_Calculus.html">11. Differential Calculus</a></li>
<li class="toctree-l1"><a class="reference internal" href="C12_Integration_and_Measure_Theory.html">12. Integration and Measure Theory</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="genindex.html">Index</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">Mathematics in Lean</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home" aria-label="Home"></a></li>
      <li class="breadcrumb-item active"><span class="section-number">5. </span>Elementary Number Theory</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/C05_Elementary_Number_Theory.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="elementary-number-theory">
<span id="number-theory"></span><h1><span class="section-number">5. </span>Elementary Number Theory<a class="headerlink" href="#elementary-number-theory" title="Link to this heading">&#61633;</a></h1>
<p>In this chapter, we show you how to formalize some elementary
results in number theory.
As we deal with more substantive mathematical content,
the proofs will get longer and more involved,
building on the skills you have already mastered.</p>
<section id="irrational-roots">
<span id="section-irrational-roots"></span><h2><span class="section-number">5.1. </span>Irrational Roots<a class="headerlink" href="#irrational-roots" title="Link to this heading">&#61633;</a></h2>
<p>Let&#8217;s start with a fact known to the ancient Greeks, namely,
that the square root of 2 is irrational.
If we suppose otherwise,
we can write <span class="math notranslate nohighlight">\(\sqrt{2} = a / b\)</span> as a fraction
in lowest terms. Squaring both sides yields <span class="math notranslate nohighlight">\(a^2 = 2 b^2\)</span>,
which implies that <span class="math notranslate nohighlight">\(a\)</span> is even.
If we write <span class="math notranslate nohighlight">\(a = 2c\)</span>, then we get <span class="math notranslate nohighlight">\(4c^2 = 2 b^2\)</span>
and hence <span class="math notranslate nohighlight">\(b^2 = 2 c^2\)</span>.
This implies that <span class="math notranslate nohighlight">\(b\)</span> is also even, contradicting
the fact that we have assumed that <span class="math notranslate nohighlight">\(a / b\)</span> has been
reduced to lowest terms.</p>
<p>Saying that <span class="math notranslate nohighlight">\(a / b\)</span> is a fraction in lowest terms means
that <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> do not have any factors in common,
which is to say, they are <em>coprime</em>.
Mathlib defines the predicate <code class="docutils literal notranslate"><span class="pre">Nat.Coprime</span> <span class="pre">m</span> <span class="pre">n</span></code> to be <code class="docutils literal notranslate"><span class="pre">Nat.gcd</span> <span class="pre">m</span> <span class="pre">n</span> <span class="pre">=</span> <span class="pre">1</span></code>.
Using Lean&#8217;s anonymous projection notation, if <code class="docutils literal notranslate"><span class="pre">s</span></code> and <code class="docutils literal notranslate"><span class="pre">t</span></code> are
expressions of type <code class="docutils literal notranslate"><span class="pre">Nat</span></code>, we can write <code class="docutils literal notranslate"><span class="pre">s.Coprime</span> <span class="pre">t</span></code> instead of
<code class="docutils literal notranslate"><span class="pre">Nat.Coprime</span> <span class="pre">s</span> <span class="pre">t</span></code>, and similarly for <code class="docutils literal notranslate"><span class="pre">Nat.gcd</span></code>.
As usual, Lean will often unfold the definition of <code class="docutils literal notranslate"><span class="pre">Nat.Coprime</span></code> automatically
when necessary,
but we can also do it manually by rewriting or simplifying with
the identifier <code class="docutils literal notranslate"><span class="pre">Nat.Coprime</span></code>.
The <code class="docutils literal notranslate"><span class="pre">norm_num</span></code> tactic is smart enough to compute concrete values.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#print</span><span class="w"> </span><span class="n">Nat.Coprime</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m.Coprime</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m.gcd</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">h</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m.Coprime</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m.gcd</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Nat.Coprime</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">exact</span><span class="w"> </span><span class="n">h</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.Coprime</span><span class="w"> </span><span class="mi">12</span><span class="w"> </span><span class="mi">7</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.gcd</span><span class="w"> </span><span class="mi">12</span><span class="w"> </span><span class="mi">8</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span>
</pre></div>
</div>
<p>We have already encountered the <code class="docutils literal notranslate"><span class="pre">gcd</span></code> function in
<a class="reference internal" href="C02_Basics.html#more-on-order-and-divisibility"><span class="std std-numref">Section 2.4</span></a>.
There is also a version of <code class="docutils literal notranslate"><span class="pre">gcd</span></code> for the integers;
we will return to a discussion of the relationship between
different number systems below.
There are even a generic <code class="docutils literal notranslate"><span class="pre">gcd</span></code> function and generic
notions of <code class="docutils literal notranslate"><span class="pre">Prime</span></code> and <code class="docutils literal notranslate"><span class="pre">Coprime</span></code>
that make sense in general classes of algebraic structures.
We will come to understand how Lean manages this generality
in the next chapter.
In the meanwhile, in this section, we will restrict attention
to the natural numbers.</p>
<p>We also need the notion of a prime number, <code class="docutils literal notranslate"><span class="pre">Nat.Prime</span></code>.
The theorem <code class="docutils literal notranslate"><span class="pre">Nat.prime_def_lt</span></code> provides one familiar characterization,
and <code class="docutils literal notranslate"><span class="pre">Nat.Prime.eq_one_or_self_of_dvd</span></code> provides another.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">Nat.prime_def_lt</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">prime_p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="n">p</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rwa</span><span class="w"> </span><span class="o">[</span><span class="n">Nat.prime_def_lt</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">prime_p</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Nat.Prime.eq_one_or_self_of_dvd</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">prime_p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="n">p</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">&#8744;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">prime_p.eq_one_or_self_of_dvd</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="mi">17</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span>

<span class="c1">-- commonly used</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Nat.prime_two</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Nat.prime_three</span>
</pre></div>
</div>
<p>In the natural numbers, a prime number has the property that it cannot
be written as a product of nontrivial factors.
In a broader mathematical context, an element of a ring that has this property
is said to be <em>irreducible</em>.
An element of a ring is said to be <em>prime</em> if whenever it divides a product,
it divides one of the factors.
It is an important property of the natural numbers
that in that setting the two notions coincide,
giving rise to the theorem <code class="docutils literal notranslate"><span class="pre">Nat.Prime.dvd_mul</span></code>.</p>
<p>We can use this fact to establish a key property in the argument
above:
if the square of a number is even, then that number is even as well.
Mathlib defines the predicate <code class="docutils literal notranslate"><span class="pre">Even</span></code> in <code class="docutils literal notranslate"><span class="pre">Algebra.Group.Even</span></code>,
but for reasons that will become clear below,
we will simply use <code class="docutils literal notranslate"><span class="pre">2</span> <span class="pre">&#8739;</span> <span class="pre">m</span></code> to express that <code class="docutils literal notranslate"><span class="pre">m</span></code> is even.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">Nat.Prime.dvd_mul</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Nat.Prime.dvd_mul</span><span class="w"> </span><span class="n">Nat.prime_two</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Nat.prime_two.dvd_mul</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">even_of_even_sqr</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">pow_two</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.prime_two.dvd_mul</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">cases</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">assumption</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Nat.Prime.dvd_of_dvd_pow</span><span class="w"> </span><span class="n">Nat.prime_two</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>As we proceed, you will need to become proficient at finding the facts you
need.
Remember that if you can guess the prefix of the name and
you have imported the relevant library,
you can use tab completion (sometimes with <code class="docutils literal notranslate"><span class="pre">ctrl-tab</span></code>) to find
what you are looking for.
You can use <code class="docutils literal notranslate"><span class="pre">ctrl-click</span></code> on any identifier to jump to the file
where it is defined, which enables you to browse definitions and theorems
nearby.
You can also use the search engine on the
<a class="reference external" href="https://leanprover-community.github.io/">Lean community web pages</a>,
and if all else fails,
don&#8217;t hesitate to ask on
<a class="reference external" href="https://leanprover.zulipchat.com/">Zulip</a>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="c1">-- apply? suggests the following:</span>
<span class="w">  </span><span class="o">(</span><span class="n">mul_right_inj&#39;</span><span class="w"> </span><span class="n">h&#39;</span><span class="o">)</span><span class="bp">.</span><span class="n">mp</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>The heart of our proof of the irrationality of the square root of two
is contained in the following theorem.
See if you can fill out the proof sketch, using
<code class="docutils literal notranslate"><span class="pre">even_of_even_sqr</span></code> and the theorem <code class="docutils literal notranslate"><span class="pre">Nat.dvd_gcd</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">coprime_mn</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m.Coprime</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">sqr_eq</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">obtain</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span><span class="w"> </span><span class="n">meq</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">dvd_iff_exists_eq_mul_left.mp</span><span class="w"> </span><span class="n">this</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">sqr_eq</span><span class="o">,</span><span class="w"> </span><span class="n">meq</span><span class="o">]</span>
<span class="w">    </span><span class="n">ring</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">m.gcd</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">norm_num</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">this</span>
</pre></div>
</div>
<p>In fact, with very few changes, we can replace <code class="docutils literal notranslate"><span class="pre">2</span></code> by an arbitrary prime.
Give it a try in the next example.
At the end of the proof, you&#8217;ll need to derive a contradiction from
<code class="docutils literal notranslate"><span class="pre">p</span> <span class="pre">&#8739;</span> <span class="pre">1</span></code>.
You can use <code class="docutils literal notranslate"><span class="pre">Nat.Prime.two_le</span></code>, which says that
any prime number is greater than or equal to two,
and <code class="docutils literal notranslate"><span class="pre">Nat.le_of_dvd</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">coprime_mn</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m.Coprime</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">prime_p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p.Prime</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Let us consider another approach.
Here is a quick proof that if <span class="math notranslate nohighlight">\(p\)</span> is prime, then
<span class="math notranslate nohighlight">\(m^2 \ne p n^2\)</span>: if we assume <span class="math notranslate nohighlight">\(m^2 = p n^2\)</span>
and consider the factorization of <span class="math notranslate nohighlight">\(m\)</span> and <span class="math notranslate nohighlight">\(n\)</span> into primes,
then <span class="math notranslate nohighlight">\(p\)</span> occurs an even number of times on the left side of the equation
and an odd number of times on the right, a contradiction.
Note that this argument requires that <span class="math notranslate nohighlight">\(n\)</span> and hence <span class="math notranslate nohighlight">\(m\)</span>
are not equal to zero.
The formalization below confirms that this assumption is sufficient.</p>
<p>The unique factorization theorem says that any natural number other
than zero can be written as the product of primes in a unique way.
Mathlib contains a formal version of this, expressed in terms of a function
<code class="docutils literal notranslate"><span class="pre">Nat.primeFactorsList</span></code>, which returns the list of
prime factors of a number in nondecreasing order.
The library proves that all the elements of <code class="docutils literal notranslate"><span class="pre">Nat.primeFactorsList</span> <span class="pre">n</span></code>
are prime, that any <code class="docutils literal notranslate"><span class="pre">n</span></code> greater than zero is equal to the
product of its factors,
and that if <code class="docutils literal notranslate"><span class="pre">n</span></code> is equal to the product of another list of prime numbers,
then that list is a permutation of <code class="docutils literal notranslate"><span class="pre">Nat.primeFactorsList</span> <span class="pre">n</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">Nat.primeFactorsList</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Nat.prime_of_mem_primeFactorsList</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Nat.prod_primeFactorsList</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Nat.primeFactorsList_unique</span>
</pre></div>
</div>
<p>You can browse these theorems and others nearby, even though we have not
talked about list membership, products, or permutations yet.
We won&#8217;t need any of that for the task at hand.
We will instead use the fact that Mathlib has a function <code class="docutils literal notranslate"><span class="pre">Nat.factorization</span></code>,
that represents the same data as a function.
Specifically, <code class="docutils literal notranslate"><span class="pre">Nat.factorization</span> <span class="pre">n</span> <span class="pre">p</span></code>, which we can also write
<code class="docutils literal notranslate"><span class="pre">n.factorization</span> <span class="pre">p</span></code>, returns the multiplicity of <code class="docutils literal notranslate"><span class="pre">p</span></code> in the prime
factorization of <code class="docutils literal notranslate"><span class="pre">n</span></code>. We will use the following three facts.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">factorization_mul&#39;</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">mnez</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">nnez</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="bp">.</span><span class="n">factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">m.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">n.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Nat.factorization_mul</span><span class="w"> </span><span class="n">mnez</span><span class="w"> </span><span class="n">nnez</span><span class="o">]</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">factorization_pow&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">k</span><span class="o">)</span><span class="bp">.</span><span class="n">factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Nat.factorization_pow</span><span class="o">]</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">Nat.Prime.factorization&#39;</span><span class="w"> </span><span class="o">{</span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">prime_p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p.Prime</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">p.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">prime_p.factorization</span><span class="o">]</span>
<span class="w">  </span><span class="n">simp</span>
</pre></div>
</div>
<p>In fact, <code class="docutils literal notranslate"><span class="pre">n.factorization</span></code> is defined in Lean as a function of finite support,
which explains the strange notation you will see as you step through the
proofs above. Don&#8217;t worry about this now. For our purposes here, we can use
the three theorems above as a black box.</p>
<p>The next example shows that the simplifier is smart enough to replace
<code class="docutils literal notranslate"><span class="pre">n^2</span> <span class="pre">&#8800;</span> <span class="pre">0</span></code> by <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">&#8800;</span> <span class="pre">0</span></code>. The tactic <code class="docutils literal notranslate"><span class="pre">simpa</span></code> just calls <code class="docutils literal notranslate"><span class="pre">simp</span></code>
followed by <code class="docutils literal notranslate"><span class="pre">assumption</span></code>.</p>
<p>See if you can use the identities above to fill in the missing parts
of the proof.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">nnz</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">prime_p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p.Prime</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">sqr_eq</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">nsqr_nez</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simpa</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">eq1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.factorization</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">m.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">eq2</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">p</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="bp">.</span><span class="n">factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">m.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">eq1</span><span class="o">,</span><span class="w"> </span><span class="n">sqr_eq</span><span class="o">,</span><span class="w"> </span><span class="n">eq2</span><span class="o">]</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add_comm</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.add_mul_mod_self_left</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.mul_mod_right</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">this</span>
<span class="w">  </span><span class="n">norm_num</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">this</span>
</pre></div>
</div>
<p>A nice thing about this proof is that it also generalizes. There is
nothing special about <code class="docutils literal notranslate"><span class="pre">2</span></code>; with small changes, the proof shows that
whenever we write <code class="docutils literal notranslate"><span class="pre">m^k</span> <span class="pre">=</span> <span class="pre">r</span> <span class="pre">*</span> <span class="pre">n^k</span></code>, the multiplicity of any prime <code class="docutils literal notranslate"><span class="pre">p</span></code>
in <code class="docutils literal notranslate"><span class="pre">r</span></code> has to be a multiple of <code class="docutils literal notranslate"><span class="pre">k</span></code>.</p>
<p>To use <code class="docutils literal notranslate"><span class="pre">Nat.count_factors_mul_of_pos</span></code> with <code class="docutils literal notranslate"><span class="pre">r</span> <span class="pre">*</span> <span class="pre">n^k</span></code>,
we need to know that <code class="docutils literal notranslate"><span class="pre">r</span></code> is positive.
But when <code class="docutils literal notranslate"><span class="pre">r</span></code> is zero, the theorem below is trivial, and easily
proved by the simplifier.
So the proof is carried out in cases.
The line <code class="docutils literal notranslate"><span class="pre">rcases</span> <span class="pre">r</span> <span class="pre">with</span> <span class="pre">_</span> <span class="pre">|</span> <span class="pre">r</span></code> replaces the goal with two versions:
one in which <code class="docutils literal notranslate"><span class="pre">r</span></code> is replaced by <code class="docutils literal notranslate"><span class="pre">0</span></code>,
and the other in which <code class="docutils literal notranslate"><span class="pre">r</span></code> is replaces by <code class="docutils literal notranslate"><span class="pre">r</span> <span class="pre">+</span> <span class="pre">1</span></code>.
In the second case, we can use the theorem <code class="docutils literal notranslate"><span class="pre">r.succ_ne_zero</span></code>, which
establishes <code class="docutils literal notranslate"><span class="pre">r</span> <span class="pre">+</span> <span class="pre">1</span> <span class="pre">&#8800;</span> <span class="pre">0</span></code> (<code class="docutils literal notranslate"><span class="pre">succ</span></code> stands for successor).</p>
<p>Notice also that the line that begins <code class="docutils literal notranslate"><span class="pre">have</span> <span class="pre">:</span> <span class="pre">npow_nz</span></code> provides a
short proof-term proof of <code class="docutils literal notranslate"><span class="pre">n^k</span> <span class="pre">&#8800;</span> <span class="pre">0</span></code>.
To understand how it works, try replacing it with a tactic proof,
and then think about how the tactics describe the proof term.</p>
<p>See if you can fill in the missing parts of the proof below.
At the very end, you can use <code class="docutils literal notranslate"><span class="pre">Nat.dvd_sub'</span></code> and <code class="docutils literal notranslate"><span class="pre">Nat.dvd_mul_right</span></code>
to finish it off.</p>
<p>Note that this example does not assume that <code class="docutils literal notranslate"><span class="pre">p</span></code> is prime, but the
conclusion is trivial when <code class="docutils literal notranslate"><span class="pre">p</span></code> is not prime since <code class="docutils literal notranslate"><span class="pre">r.factorization</span> <span class="pre">p</span></code>
is then zero by definition, and the proof works in all cases anyway.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">nnz</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">pow_eq</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">k</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">r.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="n">r</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">npow_nz</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">npowz</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">nnz</span><span class="w"> </span><span class="o">(</span><span class="n">pow_eq_zero</span><span class="w"> </span><span class="n">npowz</span><span class="o">)</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">eq1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">k</span><span class="o">)</span><span class="bp">.</span><span class="n">factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">m.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">eq2</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">((</span><span class="n">r</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">k</span><span class="o">)</span><span class="bp">.</span><span class="n">factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span>
<span class="w">      </span><span class="n">k</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="bp">.</span><span class="n">factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">r.succ.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">m.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">eq1</span><span class="o">,</span><span class="w"> </span><span class="n">pow_eq</span><span class="o">,</span><span class="w"> </span><span class="n">eq2</span><span class="o">,</span><span class="w"> </span><span class="n">add_comm</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.add_sub_cancel</span><span class="o">]</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">this</span><span class="o">]</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>There are a number of ways in which we might want to improve on these results.
To start with, a proof that the square root of two is irrational
should say something about the square root of two,
which can be understood as an element of the
real or complex numbers.
And stating that it is irrational should say something about the
rational numbers, namely, that no rational number is equal to it.
Moreover, we should extend the theorems in this section to the integers.
Although it is mathematically obvious that if we could write the square root of
two as a quotient of two integers then we could write it as a quotient
of two natural numbers,
proving this formally requires some effort.</p>
<p>In Mathlib, the natural numbers, the integers, the rationals, the reals,
and the complex numbers are represented by separate data types.
Restricting attention to the separate domains is often helpful:
we will see that it is easy to do induction on the natural numbers,
and it is easiest to reason about divisibility of integers when the
real numbers are not part of the picture.
But having to mediate between the different domains is a headache,
one we will have to contend with.
We will return to this issue later in this chapter.</p>
<p>We should also expect to be able to strengthen the conclusion of the
last theorem to say that the number <code class="docutils literal notranslate"><span class="pre">r</span></code> is a <code class="docutils literal notranslate"><span class="pre">k</span></code>-th power,
since its <code class="docutils literal notranslate"><span class="pre">k</span></code>-th root is just the product of each prime dividing <code class="docutils literal notranslate"><span class="pre">r</span></code>
raised to its multiplicity in <code class="docutils literal notranslate"><span class="pre">r</span></code> divided by <code class="docutils literal notranslate"><span class="pre">k</span></code>.
To be able to do that we will need better means for reasoning about
products and sums over a finite set,
which is also a topic we will return to.</p>
<p>In fact, the results in this section are all established in much
greater generality in Mathlib,
in <code class="docutils literal notranslate"><span class="pre">Data.Real.Irrational</span></code>.
The notion of <code class="docutils literal notranslate"><span class="pre">multiplicity</span></code> is defined for an
arbitrary commutative monoid,
and that it takes values in the extended natural numbers <code class="docutils literal notranslate"><span class="pre">enat</span></code>,
which adds the value infinity to the natural numbers.
In the next chapter, we will begin to develop the means to
appreciate the way that Lean supports this sort of generality.</p>
</section>
<section id="induction-and-recursion">
<span id="section-induction-and-recursion"></span><h2><span class="section-number">5.2. </span>Induction and Recursion<a class="headerlink" href="#induction-and-recursion" title="Link to this heading">&#61633;</a></h2>
<p>The set of natural numbers <span class="math notranslate nohighlight">\(\mathbb{N} = \{ 0, 1, 2, \ldots \}\)</span>
is not only fundamentally important in its own right,
but also a plays a central role in the construction of new mathematical objects.
Lean&#8217;s foundation allows us to declare <em>inductive types</em>,
which are types generated inductively by a given list of
<em>constructors</em>.
In Lean, the natural numbers are declared as follows.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">inductive</span><span class="w"> </span><span class="n">Nat</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span>
</pre></div>
</div>
<p>You can find this in the library by writing <code class="docutils literal notranslate"><span class="pre">#check</span> <span class="pre">Nat</span></code> and
then using <code class="docutils literal notranslate"><span class="pre">ctrl-click</span></code> on the identifier <code class="docutils literal notranslate"><span class="pre">Nat</span></code>.
The command specifies that <code class="docutils literal notranslate"><span class="pre">Nat</span></code> is the datatype generated
freely and inductively by the two constructors <code class="docutils literal notranslate"><span class="pre">zero</span> <span class="pre">:</span> <span class="pre">Nat</span></code> and
<code class="docutils literal notranslate"><span class="pre">succ</span> <span class="pre">:</span> <span class="pre">Nat</span> <span class="pre">&#8594;</span> <span class="pre">Nat</span></code>.
Of course, the library introduces notation <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code> and <code class="docutils literal notranslate"><span class="pre">0</span></code> for
<code class="docutils literal notranslate"><span class="pre">nat</span></code> and <code class="docutils literal notranslate"><span class="pre">zero</span></code> respectively. (Numerals are translated to binary
representations, but we don&#8217;t have to worry about the details of that now.)</p>
<p>What &#8220;freely&#8221; means for the working mathematician is that the type
<code class="docutils literal notranslate"><span class="pre">Nat</span></code> has an element <code class="docutils literal notranslate"><span class="pre">zero</span></code> and an injective successor function
<code class="docutils literal notranslate"><span class="pre">succ</span></code> whose image does not include <code class="docutils literal notranslate"><span class="pre">zero</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n.succ</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">Nat.zero</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Nat.succ_ne_zero</span><span class="w"> </span><span class="n">n</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m.succ</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n.succ</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Nat.succ.inj</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>What the word &#8220;inductively&#8221; means for the working mathematician is that
the natural numbers comes with a principle of proof by induction
and a principle of definition by recursion.
This section will show you how to use these.</p>
<p>Here is an example of a recursive definition of the factorial
function.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8469;</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="mi">1</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span>
</pre></div>
</div>
<p>The syntax takes some getting used to.
Notice that there is no <code class="docutils literal notranslate"><span class="pre">:=</span></code> on the first line.
The next two lines provide the base case and inductive step
for a recursive definition.
These equations hold definitionally, but they can also
be used manually by giving the name <code class="docutils literal notranslate"><span class="pre">fac</span></code> to <code class="docutils literal notranslate"><span class="pre">simp</span></code> or <code class="docutils literal notranslate"><span class="pre">rw</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>
</pre></div>
</div>
<p>The factorial function is actually already defined in Mathlib as
<code class="docutils literal notranslate"><span class="pre">Nat.factorial</span></code>. Once again, you can jump to it by typing
<code class="docutils literal notranslate"><span class="pre">#check</span> <span class="pre">Nat.factorial</span></code> and using <code class="docutils literal notranslate"><span class="pre">ctrl-click.</span></code>
For illustrative purposes, we will continue using <code class="docutils literal notranslate"><span class="pre">fac</span></code> in the examples.
The annotation <code class="docutils literal notranslate"><span class="pre">&#64;[simp]</span></code> before the definition
of <code class="docutils literal notranslate"><span class="pre">Nat.factorial</span></code> specifies that
the defining equation should be added to the database of identities
that the simplifier uses by default.</p>
<p>The principle of induction says that we can prove a general statement
about the natural numbers by proving that the statement holds of 0
and that whenever it holds of a natural number <span class="math notranslate nohighlight">\(n\)</span>,
it also holds of <span class="math notranslate nohighlight">\(n + 1\)</span>.
The line <code class="docutils literal notranslate"><span class="pre">induction'</span> <span class="pre">n</span> <span class="pre">with</span> <span class="pre">n</span> <span class="pre">ih</span></code> in the proof
below therefore results in two goals:
in the first we need to prove <code class="docutils literal notranslate"><span class="pre">0</span> <span class="pre">&lt;</span> <span class="pre">fac</span> <span class="pre">0</span></code>,
and in the second we have the added assumption <code class="docutils literal notranslate"><span class="pre">ih</span> <span class="pre">:</span> <span class="pre">0</span> <span class="pre">&lt;</span> <span class="pre">fac</span> <span class="pre">n</span></code>
and a required to prove <code class="docutils literal notranslate"><span class="pre">0</span> <span class="pre">&lt;</span> <span class="pre">fac</span> <span class="pre">(n</span> <span class="pre">+</span> <span class="pre">1)</span></code>.
The phrase <code class="docutils literal notranslate"><span class="pre">with</span> <span class="pre">n</span> <span class="pre">ih</span></code> serves to name the variable and
the assumption for the inductive hypothesis,
and you can choose whatever names you want for them.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">fac_pos</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>
<span class="w">    </span><span class="n">exact</span><span class="w"> </span><span class="n">zero_lt_one</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>
<span class="w">  </span><span class="n">exact</span><span class="w"> </span><span class="n">mul_pos</span><span class="w"> </span><span class="n">n.succ_pos</span><span class="w"> </span><span class="n">ih</span>
</pre></div>
</div>
<p>The <code class="docutils literal notranslate"><span class="pre">induction</span></code> tactic is smart enough to include hypotheses
that depend on the induction variable as part of the
induction hypothesis.
Step through the next example to see what is going on.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">dvd_fac</span><span class="w"> </span><span class="o">{</span><span class="n">i</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">ipos</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">ile</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">exact</span><span class="w"> </span><span class="n">absurd</span><span class="w"> </span><span class="n">ipos</span><span class="w"> </span><span class="o">(</span><span class="n">not_lt_of_ge</span><span class="w"> </span><span class="n">ile</span><span class="o">)</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">Nat.of_le_succ</span><span class="w"> </span><span class="n">ile</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">dvd_mul_of_dvd_right</span><span class="w"> </span><span class="o">(</span><span class="n">ih</span><span class="w"> </span><span class="n">h</span><span class="o">)</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">h</span><span class="o">]</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">dvd_mul_right</span>
</pre></div>
</div>
<p>The following example provides a crude lower bound for the factorial
function.
It turns out to be easier to start with a proof by cases,
so that the remainder of the proof starts with the case
<span class="math notranslate nohighlight">\(n = 1\)</span>.
See if you can complete the argument with a proof by induction using <code class="docutils literal notranslate"><span class="pre">pow_succ</span></code>
or <code class="docutils literal notranslate"><span class="pre">pow_succ'</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">pow_two_le_fac</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="n">n</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Induction is often used to prove identities involving finite sums and
products.
Mathlib defines the expressions <code class="docutils literal notranslate"><span class="pre">Finset.sum</span> <span class="pre">s</span> <span class="pre">f</span></code> where
<code class="docutils literal notranslate"><span class="pre">s</span> <span class="pre">:</span> <span class="pre">Finset</span> <span class="pre">&#945;</span></code> is a finite set of elements of the type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> and
<code class="docutils literal notranslate"><span class="pre">f</span></code> is a function defined on <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>.
The codomain of <code class="docutils literal notranslate"><span class="pre">f</span></code> can be any type that supports a commutative,
associative addition operation with a zero element.
If you import <code class="docutils literal notranslate"><span class="pre">Algebra.BigOperators.Basic</span></code> and issue the command
<code class="docutils literal notranslate"><span class="pre">open</span> <span class="pre">BigOperators</span></code>, you can use the more suggestive notation
<code class="docutils literal notranslate"><span class="pre">&#8721;</span> <span class="pre">x</span> <span class="pre">in</span> <span class="pre">s,</span> <span class="pre">f</span> <span class="pre">x</span></code>. Of course, there is an analogous operation and
notation for finite products.</p>
<p>We will talk about the <code class="docutils literal notranslate"><span class="pre">Finset</span></code> type and the operations
it supports in the next section, and again in a later chapter.
For now, we will only make use
of <code class="docutils literal notranslate"><span class="pre">Finset.range</span> <span class="pre">n</span></code>, which is the finite set of natural numbers
less than <code class="docutils literal notranslate"><span class="pre">n</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Finset.sum</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">f</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Finset.prod</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">f</span>

<span class="kn">open</span><span class="w"> </span><span class="n">BigOperators</span>
<span class="kn">open</span><span class="w"> </span><span class="n">Finset</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">s.sum</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">s.prod</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">range</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="bp">.</span><span class="n">sum</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">range</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="bp">.</span><span class="n">prod</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p>The facts <code class="docutils literal notranslate"><span class="pre">Finset.sum_range_zero</span></code> and <code class="docutils literal notranslate"><span class="pre">Finset.sum_range_succ</span></code>
provide a recursive description of summation up to <span class="math notranslate nohighlight">\(n\)</span>,
and similarly for products.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Finset.sum_range_zero</span><span class="w"> </span><span class="n">f</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">n.succ</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Finset.sum_range_succ</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">n</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Finset.prod_range_zero</span><span class="w"> </span><span class="n">f</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">n.succ</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Finset.prod_range_succ</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">n</span>
</pre></div>
</div>
<p>The first identity in each pair holds definitionally, which is to say,
you can replace the proofs by <code class="docutils literal notranslate"><span class="pre">rfl</span></code>.</p>
<p>The following expresses the factorial function that we defined as a product.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="o">(</span><span class="n">i</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">,</span><span class="w"> </span><span class="n">prod_range_zero</span><span class="o">]</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">,</span><span class="w"> </span><span class="n">ih</span><span class="o">,</span><span class="w"> </span><span class="n">prod_range_succ</span><span class="o">,</span><span class="w"> </span><span class="n">mul_comm</span><span class="o">]</span>
</pre></div>
</div>
<p>The fact that we include <code class="docutils literal notranslate"><span class="pre">mul_comm</span></code> as a simplification rule deserves
comment.
It should seem dangerous to simplify with the identity <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">*</span> <span class="pre">y</span> <span class="pre">=</span> <span class="pre">y</span> <span class="pre">*</span> <span class="pre">x</span></code>,
which would ordinarily loop indefinitely.
Lean&#8217;s simplifier is smart enough to recognize that, and applies the rule
only in the case where the resulting term has a smaller value in some
fixed but arbitrary ordering of the terms.
The following example shows that simplifying using the three rules
<code class="docutils literal notranslate"><span class="pre">mul_assoc</span></code>, <code class="docutils literal notranslate"><span class="pre">mul_comm</span></code>, and <code class="docutils literal notranslate"><span class="pre">mul_left_comm</span></code>
manages to identify products that are the same up to the
placement of parentheses and ordering of variables.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">d</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">e</span><span class="o">))</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">e</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">mul_assoc</span><span class="o">,</span><span class="w"> </span><span class="n">mul_comm</span><span class="o">,</span><span class="w"> </span><span class="n">mul_left_comm</span><span class="o">]</span>
</pre></div>
</div>
<p>Roughly, the rules work by pushing parentheses to the right
and then re-ordering the expressions on both sides until they
both follow the same canonical order. Simplifying with these
rules, and the corresponding rules for addition, is a handy trick.</p>
<p>Returning to summation identities, we suggest stepping through the following proof
that the sum of the natural numbers up to and including <span class="math notranslate nohighlight">\(n\)</span> is
<span class="math notranslate nohighlight">\(n (n + 1) / 2\)</span>.
The first step of the proof clears the denominator.
This is generally useful when formalizing identities,
because calculations with division generally have side conditions.
(It is similarly useful to avoid using subtraction on the natural numbers when possible.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">sum_id</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">),</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">symm</span><span class="bp">;</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">Nat.div_eq_of_eq_mul_right</span><span class="w"> </span><span class="o">(</span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Finset.sum_range_succ</span><span class="o">,</span><span class="w"> </span><span class="n">mul_add</span><span class="w"> </span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">ih</span><span class="o">]</span>
<span class="w">  </span><span class="n">ring</span>
</pre></div>
</div>
<p>We encourage you to prove the analogous identity for sums of squares,
and other identities you can find on the web.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">sum_sqr</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">),</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">6</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>In Lean&#8217;s core library, addition and multiplication are themselves defined
using recursive definitions,
and their fundamental properties are established using induction.
If you like thinking about foundational topics like that,
you might enjoy working through proofs
of the commutativity and associativity of multiplication and addition
and the distributivity of multiplication over addition.
You can do this on a copy of the natural numbers
following the outline below.
Notice that we can use the <code class="docutils literal notranslate"><span class="pre">induction</span></code> tactic with <code class="docutils literal notranslate"><span class="pre">MyNat</span></code>;
Lean is smart enough to know to
use the relevant induction principle (which is, of course,
the same as that for <code class="docutils literal notranslate"><span class="pre">Nat</span></code>).</p>
<p>We start you off with the commutativity of addition.
A good rule of thumb is that because addition and multiplication
are defined by recursion on the second argument,
it is generally advantageous to do proofs by induction on a variable
that occurs in that position.
It is a bit tricky to decide which variable to use in the proof
of associativity.</p>
<p>It can be confusing to write things without the usual notation
for zero, one, addition, and multiplication.
We will learn how to define such notation later.
Working in the namespace <code class="docutils literal notranslate"><span class="pre">MyNat</span></code> means that we can write
<code class="docutils literal notranslate"><span class="pre">zero</span></code> and <code class="docutils literal notranslate"><span class="pre">succ</span></code> rather than <code class="docutils literal notranslate"><span class="pre">MyNat.zero</span></code> and <code class="docutils literal notranslate"><span class="pre">MyNat.succ</span></code>,
and that these interpretations of the names take precedence over
others.
Outside the namespace, the full name of the <code class="docutils literal notranslate"><span class="pre">add</span></code> defined below,
for example, is <code class="docutils literal notranslate"><span class="pre">MyNat.add</span></code>.</p>
<p>If you find that you <em>really</em> enjoy this sort of thing, try defining
truncated subtraction and exponentiation and proving some of their
properties as well.
Remember that truncated subtraction cuts off at zero.
To define that, it is useful to define a predecessor function, <code class="docutils literal notranslate"><span class="pre">pred</span></code>,
that subtracts one from any nonzero number and fixes zero.
The function <code class="docutils literal notranslate"><span class="pre">pred</span></code> can be defined by a simple instance of recursion.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">inductive</span><span class="w"> </span><span class="n">MyNat</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">MyNat</span>

<span class="kn">namespace</span><span class="w"> </span><span class="n">MyNat</span>

<span class="kd">def</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">MyNat</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">MyNat</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="o">(</span><span class="n">add</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="o">)</span>

<span class="kd">def</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">MyNat</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">MyNat</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">zero</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="o">(</span><span class="n">mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="n">x</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">zero_add</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">rfl</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add</span><span class="o">,</span><span class="w"> </span><span class="n">ih</span><span class="o">]</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">succ_add</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="o">(</span><span class="n">succ</span><span class="w"> </span><span class="n">m</span><span class="o">)</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="o">(</span><span class="n">add</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">rfl</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add</span><span class="o">,</span><span class="w"> </span><span class="n">ih</span><span class="o">]</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">add_comm</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">zero_add</span><span class="o">]</span>
<span class="w">    </span><span class="n">rfl</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add</span><span class="o">,</span><span class="w"> </span><span class="n">succ_add</span><span class="o">,</span><span class="w"> </span><span class="n">ih</span><span class="o">]</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">add_assoc</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="o">(</span><span class="n">add</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">(</span><span class="n">add</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">k</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">mul_add</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">(</span><span class="n">add</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">k</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="o">(</span><span class="n">mul</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">mul</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">k</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">zero_mul</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">succ_mul</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="o">(</span><span class="n">succ</span><span class="w"> </span><span class="n">m</span><span class="o">)</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="o">(</span><span class="n">mul</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">mul_comm</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">end</span><span class="w"> </span><span class="n">MyNat</span>
</pre></div>
</div>
</section>
<section id="infinitely-many-primes">
<span id="section-infinitely-many-primes"></span><h2><span class="section-number">5.3. </span>Infinitely Many Primes<a class="headerlink" href="#infinitely-many-primes" title="Link to this heading">&#61633;</a></h2>
<p>Let us continue our exploration of induction and recursion with another
mathematical standard: a proof that there are infinitely many primes.
One way to formulate this is as the statement that
for every natural number
<span class="math notranslate nohighlight">\(n\)</span>, there is a prime number greater than <span class="math notranslate nohighlight">\(n\)</span>.
To prove this, let <span class="math notranslate nohighlight">\(p\)</span> be any prime factor of <span class="math notranslate nohighlight">\(n! + 1\)</span>.
If <span class="math notranslate nohighlight">\(p\)</span> is less than or equal to <span class="math notranslate nohighlight">\(n\)</span>, it divides <span class="math notranslate nohighlight">\(n!\)</span>.
Since it also divides <span class="math notranslate nohighlight">\(n! + 1\)</span>, it divides 1, a contradiction.
Hence <span class="math notranslate nohighlight">\(p\)</span> is greater than <span class="math notranslate nohighlight">\(n\)</span>.</p>
<p>To formalize that proof, we need to show that any number greater than or equal
to 2 has a prime factor.
To do that, we will need to show that any natural number that is
not equal to 0 or 1 is greater-than or equal to 2.
And this brings us to a quirky feature of formalization:
it is often trivial statements like this that are among the most
annoying to formalize.
Here we consider a few ways to do it.</p>
<p>To start with, we can use the <code class="docutils literal notranslate"><span class="pre">cases</span></code> tactic and the fact that the
successor function respects the ordering on the natural numbers.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">two_le</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h0</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">cases</span><span class="w"> </span><span class="n">m</span><span class="bp">;</span><span class="w"> </span><span class="n">contradiction</span>
<span class="w">  </span><span class="n">case</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">    </span><span class="n">cases</span><span class="w"> </span><span class="n">m</span><span class="bp">;</span><span class="w"> </span><span class="n">contradiction</span>
<span class="w">    </span><span class="n">repeat</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">Nat.succ_le_succ</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">zero_le</span>
</pre></div>
</div>
<p>Another strategy is to use the tactic <code class="docutils literal notranslate"><span class="pre">interval_cases</span></code>,
which automatically splits the goal into cases when
the variable in question is contained in an interval
of natural numbers or integers.
Remember that you can hover over it to see its documentation.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h0</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">by_contra</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">push_neg</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">interval_cases</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">contradiction</span>
</pre></div>
</div>
<p id="index-0">Recall that the semicolon after <code class="docutils literal notranslate"><span class="pre">interval_cases</span> <span class="pre">m</span></code> means
that the next tactic is applied to each of the cases that it generates.
Yet another option is to use the tactic <code class="docutils literal notranslate"><span class="pre">decide</span></code>, which tries
to find a decision procedure to solve the problem.
Lean knows that you can decide the truth value of a statement that
begins with a bounded quantifier <code class="docutils literal notranslate"><span class="pre">&#8704;</span> <span class="pre">x,</span> <span class="pre">x</span> <span class="pre">&lt;</span> <span class="pre">n</span> <span class="pre">&#8594;</span> <span class="pre">...</span></code> or <code class="docutils literal notranslate"><span class="pre">&#8707;</span> <span class="pre">x,</span> <span class="pre">x</span> <span class="pre">&lt;</span> <span class="pre">n</span> <span class="pre">&#8743;</span> <span class="pre">...</span></code>
by deciding each of the finitely many instances.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h0</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">by_contra</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">push_neg</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">revert</span><span class="w"> </span><span class="n">h0</span><span class="w"> </span><span class="n">h1</span>
<span class="w">  </span><span class="n">revert</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="n">m</span>
<span class="w">  </span><span class="n">decide</span>
</pre></div>
</div>
<p>With the theorem <code class="docutils literal notranslate"><span class="pre">two_le</span></code> in hand, let&#8217;s start by showing that every
natural number greater than two has a prime divisor.
Mathlib contains a function <code class="docutils literal notranslate"><span class="pre">Nat.minFac</span></code> that
returns the smallest prime divisor,
but for the sake of learning new parts of the library,
we&#8217;ll avoid using it and prove the theorem directly.</p>
<p>Here, ordinary induction isn&#8217;t enough.
We want to use <em>strong induction</em>, which allows us to prove
that every natural number <span class="math notranslate nohighlight">\(n\)</span> has a property <span class="math notranslate nohighlight">\(P\)</span>
by showing that for every number <span class="math notranslate nohighlight">\(n\)</span>, if <span class="math notranslate nohighlight">\(P\)</span> holds
of all values less than <span class="math notranslate nohighlight">\(n\)</span>, it holds at <span class="math notranslate nohighlight">\(n\)</span> as well.
In Lean, this principle is called <code class="docutils literal notranslate"><span class="pre">Nat.strong_induction_on</span></code>,
and we can use the <code class="docutils literal notranslate"><span class="pre">using</span></code> keyword to tell the induction tactic
to use it.
Notice that when we do that, there is no base case; it is subsumed
by the general induction step.</p>
<p>The argument is simply as follows. Assuming <span class="math notranslate nohighlight">\(n &#8805; 2\)</span>,
if <span class="math notranslate nohighlight">\(n\)</span> is prime, we&#8217;re done. If it isn&#8217;t,
then by one of the characterizations of what it means to be a prime number,
it has a nontrivial factor, <span class="math notranslate nohighlight">\(m\)</span>,
and we can apply the inductive hypothesis to that.
Step through the next proof to see how that plays out.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">exists_prime_factor</span><span class="w"> </span><span class="o">{</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">,</span><span class="w"> </span><span class="n">p.Prime</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">by_cases</span><span class="w"> </span><span class="n">np</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n.Prime</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">use</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">np</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">using</span><span class="w"> </span><span class="n">Nat.strong_induction_on</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Nat.prime_def_lt</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">np</span>
<span class="w">  </span><span class="n">push_neg</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">np</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">np</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">m</span><span class="o">,</span><span class="w"> </span><span class="n">mltn</span><span class="o">,</span><span class="w"> </span><span class="n">mdvdn</span><span class="o">,</span><span class="w"> </span><span class="n">mne1</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span><span class="w"> </span><span class="n">mz</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mz</span><span class="o">,</span><span class="w"> </span><span class="n">zero_dvd_iff</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">mdvdn</span>
<span class="w">    </span><span class="n">linarith</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">mgt2</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">two_le</span><span class="w"> </span><span class="n">this</span><span class="w"> </span><span class="n">mne1</span>
<span class="w">  </span><span class="n">by_cases</span><span class="w"> </span><span class="n">mp</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m.Prime</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">use</span><span class="w"> </span><span class="n">m</span><span class="o">,</span><span class="w"> </span><span class="n">mp</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">rcases</span><span class="w"> </span><span class="n">ih</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">mltn</span><span class="w"> </span><span class="n">mgt2</span><span class="w"> </span><span class="n">mp</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">pp</span><span class="o">,</span><span class="w"> </span><span class="n">pdvd</span><span class="o">&#10217;</span>
<span class="w">    </span><span class="n">use</span><span class="w"> </span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">pp</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">pdvd.trans</span><span class="w"> </span><span class="n">mdvdn</span>
</pre></div>
</div>
<p>We can now prove the following formulation of our theorem.
See if you can fill out the sketch.
You can use <code class="docutils literal notranslate"><span class="pre">Nat.factorial_pos</span></code>, <code class="docutils literal notranslate"><span class="pre">Nat.dvd_factorial</span></code>,
and <code class="docutils literal notranslate"><span class="pre">Nat.dvd_sub'</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">primes_infinite</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&gt;</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">n</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">Nat.factorial</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">exists_prime_factor</span><span class="w"> </span><span class="n">this</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">pp</span><span class="o">,</span><span class="w"> </span><span class="n">pdvd</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="n">refine</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="bp">?</span><span class="n">_</span><span class="o">,</span><span class="w"> </span><span class="n">pp</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="k">show</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&gt;</span><span class="w"> </span><span class="n">n</span>
<span class="w">  </span><span class="n">by_contra</span><span class="w"> </span><span class="n">ple</span>
<span class="w">  </span><span class="n">push_neg</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">ple</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">Nat.factorial</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">show</span><span class="w"> </span><span class="n">False</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Let&#8217;s consider a variation of the proof above, where instead
of using the factorial function,
we suppose that we are given by a finite set
<span class="math notranslate nohighlight">\(\{ p_1, \ldots, p_n \}\)</span> and we consider a prime factor of
<span class="math notranslate nohighlight">\(\prod_{i = 1}^n p_i + 1\)</span>.
That prime factor has to be distinct from each
<span class="math notranslate nohighlight">\(p_i\)</span>, showing that there is no finite set that contains
all the prime numbers.</p>
<p>Formalizing this argument requires us to reason about finite
sets. In Lean, for any type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>, the type <code class="docutils literal notranslate"><span class="pre">Finset</span> <span class="pre">&#945;</span></code>
represents finite sets of elements of type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>.
Reasoning about finite sets computationally requires having
a procedure to test equality on <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>, which is why the snippet
below includes the assumption <code class="docutils literal notranslate"><span class="pre">[DecidableEq</span> <span class="pre">&#945;]</span></code>.
For concrete data types like <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code>, <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code>, and <code class="docutils literal notranslate"><span class="pre">&#8474;</span></code>,
the assumption is satisfied automatically. When reasoning about
the real numbers, it can be satisfied using classical logic
and abandoning the computational interpretation.</p>
<p>We use the command <code class="docutils literal notranslate"><span class="pre">open</span> <span class="pre">Finset</span></code> to avail ourselves of shorter names
for the relevant theorems. Unlike the case with sets,
most equivalences involving finsets do not hold definitionally,
so they need to be expanded manually using equivalences like
<code class="docutils literal notranslate"><span class="pre">Finset.subset_iff</span></code>, <code class="docutils literal notranslate"><span class="pre">Finset.mem_union</span></code>, <code class="docutils literal notranslate"><span class="pre">Finset.mem_inter</span></code>,
and <code class="docutils literal notranslate"><span class="pre">Finset.mem_sdiff</span></code>. The <code class="docutils literal notranslate"><span class="pre">ext</span></code> tactic can still be used
to show that two finite sets are equal by showing
that every element of one is an element of the other.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Finset</span>

<span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">DecidableEq</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">t</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8838;</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">subset_iff</span><span class="o">]</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mem_inter</span><span class="o">,</span><span class="w"> </span><span class="n">mem_union</span><span class="o">,</span><span class="w"> </span><span class="n">mem_union</span><span class="o">,</span><span class="w"> </span><span class="n">mem_inter</span><span class="o">,</span><span class="w"> </span><span class="n">mem_inter</span><span class="o">]</span>
<span class="w">  </span><span class="n">tauto</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">t</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8838;</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">subset_iff</span><span class="o">]</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="n">tauto</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="bp">&#8838;</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">t</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">subset_iff</span><span class="o">]</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="n">tauto</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">t</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">ext</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="n">simp</span>
<span class="w">  </span><span class="n">tauto</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>We have used a new trick: the <code class="docutils literal notranslate"><span class="pre">tauto</span></code> tactic (and a strengthened
version, <code class="docutils literal notranslate"><span class="pre">tauto!</span></code>, which uses classical logic) can be used to
dispense with propositional tautologies. See if you can use
these methods to prove the two examples below.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">s</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">t</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="bp">\</span><span class="w"> </span><span class="n">s</span><span class="o">)</span><span class="w"> </span><span class="bp">\</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">\</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">t</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>The theorem <code class="docutils literal notranslate"><span class="pre">Finset.dvd_prod_of_mem</span></code> tells us that if an
<code class="docutils literal notranslate"><span class="pre">n</span></code> is an element of a finite set <code class="docutils literal notranslate"><span class="pre">s</span></code>, then <code class="docutils literal notranslate"><span class="pre">n</span></code> divides
<code class="docutils literal notranslate"><span class="pre">&#8719;</span> <span class="pre">i</span> <span class="pre">in</span> <span class="pre">s,</span> <span class="pre">i</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Finset.dvd_prod_of_mem</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>We also need to know that the converse holds in the case where
<code class="docutils literal notranslate"><span class="pre">n</span></code> is prime and <code class="docutils literal notranslate"><span class="pre">s</span></code> is a set of primes.
To show that, we need the following lemma, which you should
be able to prove using the theorem <code class="docutils literal notranslate"><span class="pre">Nat.Prime.eq_one_or_self_of_dvd</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">_root_.Nat.Prime.eq_of_dvd_of_prime</span><span class="w"> </span><span class="o">{</span><span class="n">p</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span>
<span class="w">      </span><span class="o">(</span><span class="n">prime_p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="n">p</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">prime_q</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="n">q</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">q</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We can use this lemma to show that if a prime <code class="docutils literal notranslate"><span class="pre">p</span></code> divides a product of a finite
set of primes, then it is equal to one of them.
Mathlib provides a useful principle of induction on finite sets:
to show that a property holds of an arbitrary finite set <code class="docutils literal notranslate"><span class="pre">s</span></code>,
show that it holds of the empty set, and show that it is preserved
when we add a single new element <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">&#8713;</span> <span class="pre">s</span></code>.
The principle is known as <code class="docutils literal notranslate"><span class="pre">Finset.induction_on</span></code>.
When we tell the induction tactic to use it, we can also specify the names
<code class="docutils literal notranslate"><span class="pre">a</span></code> and <code class="docutils literal notranslate"><span class="pre">s</span></code>, the name for the assumption <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">&#8713;</span> <span class="pre">s</span></code> in the inductive step,
and the name of the inductive hypothesis.
The expression <code class="docutils literal notranslate"><span class="pre">Finset.insert</span> <span class="pre">a</span> <span class="pre">s</span></code> denotes the union of <code class="docutils literal notranslate"><span class="pre">s</span></code> with the singleton <code class="docutils literal notranslate"><span class="pre">a</span></code>.
The identities <code class="docutils literal notranslate"><span class="pre">Finset.prod_empty</span></code> and <code class="docutils literal notranslate"><span class="pre">Finset.prod_insert</span></code> then provide
the relevant rewrite rules for the product.
In the proof below, the first <code class="docutils literal notranslate"><span class="pre">simp</span></code> applies <code class="docutils literal notranslate"><span class="pre">Finset.prod_empty</span></code>.
Step through the beginning of the proof to see the induction unfold,
and then finish it off.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">mem_of_dvd_prod_primes</span><span class="w"> </span><span class="o">{</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">prime_p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p.Prime</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="o">(</span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">h&#8320;</span><span class="w"> </span><span class="n">h&#8321;</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">using</span><span class="w"> </span><span class="n">Finset.induction_on</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">ans</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h&#8321;</span>
<span class="w">    </span><span class="n">linarith</span><span class="w"> </span><span class="o">[</span><span class="n">prime_p.two_le</span><span class="o">]</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">Finset.prod_insert</span><span class="w"> </span><span class="n">ans</span><span class="o">,</span><span class="w"> </span><span class="n">prime_p.dvd_mul</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h&#8320;</span><span class="w"> </span><span class="n">h&#8321;</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mem_insert</span><span class="o">]</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We need one last property of finite sets.
Given an element <code class="docutils literal notranslate"><span class="pre">s</span> <span class="pre">:</span> <span class="pre">Set</span> <span class="pre">&#945;</span></code> and a predicate
<code class="docutils literal notranslate"><span class="pre">P</span></code> on <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>, in  <a class="reference internal" href="C04_Sets_and_Functions.html#sets-and-functions"><span class="std std-numref">Chapter 4</span></a>
we wrote <code class="docutils literal notranslate"><span class="pre">{</span> <span class="pre">x</span> <span class="pre">&#8712;</span> <span class="pre">s</span> <span class="pre">|</span> <span class="pre">P</span> <span class="pre">x</span> <span class="pre">}</span></code> for the set of
elements of <code class="docutils literal notranslate"><span class="pre">s</span></code> that satisfy <code class="docutils literal notranslate"><span class="pre">P</span></code>.
Given <code class="docutils literal notranslate"><span class="pre">s</span> <span class="pre">:</span> <span class="pre">Finset</span> <span class="pre">&#945;</span></code>,
the analogous notion is written <code class="docutils literal notranslate"><span class="pre">s.filter</span> <span class="pre">P</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s.filter</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">x.Prime</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">mem_filter</span>
</pre></div>
</div>
<p>We now prove an alternative formulation of the statement that there are infinitely many
primes, namely, that given any <code class="docutils literal notranslate"><span class="pre">s</span> <span class="pre">:</span> <span class="pre">Finset</span> <span class="pre">&#8469;</span></code>, there is a prime <code class="docutils literal notranslate"><span class="pre">p</span></code> that is not
an element of <code class="docutils literal notranslate"><span class="pre">s</span></code>.
Aiming for a contradiction, we assume that all the primes are in <code class="docutils literal notranslate"><span class="pre">s</span></code>, and then
cut down to a set <code class="docutils literal notranslate"><span class="pre">s'</span></code> that contains all and only the primes.
Taking the product of that set, adding one, and finding a prime factor
of the result
leads to the contradiction we are looking for.
See if you can complete the sketch below.
You can use <code class="docutils literal notranslate"><span class="pre">Finset.prod_pos</span></code> in the proof of the first <code class="docutils literal notranslate"><span class="pre">have</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">primes_infinite&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">Nat</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8713;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">s</span>
<span class="w">  </span><span class="n">by_contra</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">push_neg</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">set</span><span class="w"> </span><span class="n">s&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">s.filter</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">s&#39;_def</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">mem_s&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="o">{</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">},</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s&#39;</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">n.Prime</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span><span class="w"> </span><span class="n">n</span>
<span class="w">    </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">s&#39;_def</span><span class="o">]</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">s&#39;</span><span class="o">,</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">exists_prime_factor</span><span class="w"> </span><span class="n">this</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">pp</span><span class="o">,</span><span class="w"> </span><span class="n">pdvd</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">s&#39;</span><span class="o">,</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">convert</span><span class="w"> </span><span class="n">Nat.dvd_sub&#39;</span><span class="w"> </span><span class="n">pdvd</span><span class="w"> </span><span class="n">this</span>
<span class="w">    </span><span class="n">simp</span>
<span class="w">  </span><span class="k">show</span><span class="w"> </span><span class="n">False</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We have thus seen two ways of saying that there are infinitely many primes:
saying that they are not bounded by any <code class="docutils literal notranslate"><span class="pre">n</span></code>, and saying that they are
not contained in any finite set <code class="docutils literal notranslate"><span class="pre">s</span></code>.
The two proofs below show that these formulations are equivalent.
In the second, in order to form <code class="docutils literal notranslate"><span class="pre">s.filter</span> <span class="pre">Q</span></code>, we have to assume that there
is a procedure for deciding whether or not <code class="docutils literal notranslate"><span class="pre">Q</span></code> holds. Lean knows that there
is a procedure for <code class="docutils literal notranslate"><span class="pre">Nat.Prime</span></code>. In general, if we use classical logic
by writing <code class="docutils literal notranslate"><span class="pre">open</span> <span class="pre">Classical</span></code>,
we can dispense with the assumption.</p>
<p>In Mathlib, <code class="docutils literal notranslate"><span class="pre">Finset.sup</span> <span class="pre">s</span> <span class="pre">f</span></code> denotes the supremum of the values of <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">x</span></code> as <code class="docutils literal notranslate"><span class="pre">x</span></code>
ranges over <code class="docutils literal notranslate"><span class="pre">s</span></code>, returning <code class="docutils literal notranslate"><span class="pre">0</span></code> in the case where <code class="docutils literal notranslate"><span class="pre">s</span></code> is empty and
the codomain of <code class="docutils literal notranslate"><span class="pre">f</span></code> is <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code>. In the first proof, we use <code class="docutils literal notranslate"><span class="pre">s.sup</span> <span class="pre">id</span></code>,
where <code class="docutils literal notranslate"><span class="pre">id</span></code> is the identity function, to refer to the maximum value in <code class="docutils literal notranslate"><span class="pre">s</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">bounded_of_ex_finset</span><span class="w"> </span><span class="o">(</span><span class="n">Q</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="kt">Prop</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">k</span><span class="o">,</span><span class="w"> </span><span class="n">Q</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">k</span><span class="o">,</span><span class="w"> </span><span class="n">Q</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rintro</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">hs</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="n">use</span><span class="w"> </span><span class="n">s.sup</span><span class="w"> </span><span class="n">id</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="n">Qk</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">Nat.lt_succ_of_le</span>
<span class="w">  </span><span class="k">show</span><span class="w"> </span><span class="n">id</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">s.sup</span><span class="w"> </span><span class="n">id</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">le_sup</span><span class="w"> </span><span class="o">(</span><span class="n">hs</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="n">Qk</span><span class="o">)</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">ex_finset_of_bounded</span><span class="w"> </span><span class="o">(</span><span class="n">Q</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="kt">Prop</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">DecidablePred</span><span class="w"> </span><span class="n">Q</span><span class="o">]</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">k</span><span class="o">,</span><span class="w"> </span><span class="n">Q</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">k</span><span class="o">,</span><span class="w"> </span><span class="n">Q</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rintro</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">hn</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="n">use</span><span class="w"> </span><span class="o">(</span><span class="n">range</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">))</span><span class="bp">.</span><span class="n">filter</span><span class="w"> </span><span class="n">Q</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">k</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">Nat.lt_succ_iff</span><span class="o">]</span>
<span class="w">  </span><span class="n">exact</span><span class="w"> </span><span class="n">hn</span><span class="w"> </span><span class="n">k</span>
</pre></div>
</div>
<p>A small variation on our second proof that there are infinitely many primes
shows that there are infinitely many primes congruent to 3 modulo 4.
The argument goes as follows.
First, notice that if the product of two numbers <span class="math notranslate nohighlight">\(m\)</span> and <span class="math notranslate nohighlight">\(n\)</span>
is equal to 3 modulo 4, then one of the two numbers is congruent to 3 modulo 4.
After all, both have to be odd, and if they are both congruent to 1 modulo 4,
so is their product.
We can use this observation to show that if some number
greater than 2 is congruent to 3 modulo 4,
then that number has a prime divisor that is also congruent to 3 modulo 4.</p>
<p>Now suppose there are only finitely many prime numbers congruent to 3
modulo 4, say, <span class="math notranslate nohighlight">\(p_1, \ldots, p_k\)</span>.
Without loss of generality, we can assume that <span class="math notranslate nohighlight">\(p_1 = 3\)</span>.
Consider the product <span class="math notranslate nohighlight">\(4 \prod_{i = 2}^k p_i + 3\)</span>.
It is easy to see that this is congruent to 3 modulo 4, so it has
a prime factor <span class="math notranslate nohighlight">\(p\)</span> congruent to 3 modulo 4.
It can&#8217;t be the case that <span class="math notranslate nohighlight">\(p = 3\)</span>; since <span class="math notranslate nohighlight">\(p\)</span>
divides <span class="math notranslate nohighlight">\(4 \prod_{i = 2}^k p_i + 3\)</span>, if <span class="math notranslate nohighlight">\(p\)</span>
were equal to 3 then it would also divide <span class="math notranslate nohighlight">\(\prod_{i = 2}^k p_i\)</span>,
which implies that <span class="math notranslate nohighlight">\(p\)</span> is equal to
one of the <span class="math notranslate nohighlight">\(p_i\)</span> for <span class="math notranslate nohighlight">\(i = 2, \ldots, k\)</span>;
and we have excluded 3 from this list.
So <span class="math notranslate nohighlight">\(p\)</span> has to be one of the other elements <span class="math notranslate nohighlight">\(p_i\)</span>.
But in that case, <span class="math notranslate nohighlight">\(p\)</span> divides <span class="math notranslate nohighlight">\(4 \prod_{i = 2}^k p_i\)</span>
and hence 3, which contradicts the fact that it is not 3.</p>
<p>In Lean, the notation <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">%</span> <span class="pre">m</span></code>, read &#8220;<code class="docutils literal notranslate"><span class="pre">n</span></code> modulo <code class="docutils literal notranslate"><span class="pre">m</span></code>,&#8221;
denotes the remainder of the division of <code class="docutils literal notranslate"><span class="pre">n</span></code> by <code class="docutils literal notranslate"><span class="pre">m</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">27</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span>
</pre></div>
</div>
<p>We can then render the statement &#8220;<code class="docutils literal notranslate"><span class="pre">n</span></code> is congruent to 3 modulo 4&#8221;
as <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">%</span> <span class="pre">4</span> <span class="pre">=</span> <span class="pre">3</span></code>. The following example and theorems sum up
the facts about this function that we will need to use below.
The first named theorem is another illustration of reasoning by
a small number of cases.
In the second named theorem, remember that the semicolon means that
the subsequent tactic block is applied to all the goals created by the
preceding tactic.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="mi">4</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">3</span><span class="o">)</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add_comm</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.add_mul_mod_self_left</span><span class="o">]</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">mod_4_eq_3_or_mod_4_eq_3</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="bp">&#8744;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">revert</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Nat.mul_mod</span><span class="o">]</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Nat.mod_lt</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">(</span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span><span class="o">)</span>
<span class="w">  </span><span class="n">interval_cases</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="bp">-</span><span class="n">Nat.mul_mod_mod</span><span class="o">]</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Nat.mod_lt</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">(</span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span><span class="o">)</span>
<span class="w">  </span><span class="n">interval_cases</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">two_le_of_mod_4_eq_3</span><span class="w"> </span><span class="o">{</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">two_le</span><span class="w"> </span><span class="bp">&lt;;&gt;</span>
<span class="w">    </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">intro</span><span class="w"> </span><span class="n">neq</span>
<span class="w">      </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">neq</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
<span class="w">      </span><span class="n">norm_num</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>We will also need the following fact, which says that if
<code class="docutils literal notranslate"><span class="pre">m</span></code> is a nontrivial divisor of <code class="docutils literal notranslate"><span class="pre">n</span></code>, then so is <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">/</span> <span class="pre">m</span></code>.
See if you can complete the proof using <code class="docutils literal notranslate"><span class="pre">Nat.div_dvd_of_dvd</span></code>
and <code class="docutils literal notranslate"><span class="pre">Nat.div_lt_self</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">aux</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8320;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8321;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">m</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8322;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Now put all the pieces together to prove that any
number congruent to 3 modulo 4 has a prime divisor with that
same property.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">exists_prime_factor_mod_4_eq_3</span><span class="w"> </span><span class="o">{</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">,</span><span class="w"> </span><span class="n">p.Prime</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">by_cases</span><span class="w"> </span><span class="n">np</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n.Prime</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">use</span><span class="w"> </span><span class="n">n</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">using</span><span class="w"> </span><span class="n">Nat.strong_induction_on</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Nat.prime_def_lt</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">np</span>
<span class="w">  </span><span class="n">push_neg</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">np</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">np</span><span class="w"> </span><span class="o">(</span><span class="n">two_le_of_mod_4_eq_3</span><span class="w"> </span><span class="n">h</span><span class="o">)</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">m</span><span class="o">,</span><span class="w"> </span><span class="n">mltn</span><span class="o">,</span><span class="w"> </span><span class="n">mdvdn</span><span class="o">,</span><span class="w"> </span><span class="n">mne1</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">mge2</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">two_le</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">mne1</span>
<span class="w">    </span><span class="n">intro</span><span class="w"> </span><span class="n">mz</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mz</span><span class="o">,</span><span class="w"> </span><span class="n">zero_dvd_iff</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">mdvdn</span>
<span class="w">    </span><span class="n">linarith</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">neq</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">m</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Nat.mul_div_cancel&#39;</span><span class="w"> </span><span class="n">mdvdn</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="bp">&#8744;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">mod_4_eq_3_or_mod_4_eq_3</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">neq</span><span class="o">,</span><span class="w"> </span><span class="n">h</span><span class="o">]</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">this</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">h1</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="n">h1</span>
<span class="w">  </span><span class="bp">.</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">  </span><span class="bp">.</span><span class="w"> </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We are in the home stretch. Given a set <code class="docutils literal notranslate"><span class="pre">s</span></code> of prime
numbers, we need to talk about the result of removing 3 from that
set, if it is present. The function <code class="docutils literal notranslate"><span class="pre">Finset.erase</span></code> handles that.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">erase</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rwa</span><span class="w"> </span><span class="o">[</span><span class="n">mem_erase</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">erase</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">assumption</span>
</pre></div>
</div>
<p>We are now ready to prove that there are infinitely many primes
congruent to 3 modulo 4.
Fill in the missing parts below.
Our solution uses <code class="docutils literal notranslate"><span class="pre">Nat.dvd_add_iff_left</span></code> and <code class="docutils literal notranslate"><span class="pre">Nat.dvd_sub'</span></code>
along the way.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">primes_mod_4_eq_3_infinite</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&gt;</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">by_contra</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">push_neg</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">hn</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">Nat</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="n">p.Prime</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">ex_finset_of_bounded</span>
<span class="w">    </span><span class="n">use</span><span class="w"> </span><span class="n">n</span>
<span class="w">    </span><span class="n">contrapose</span><span class="bp">!</span><span class="w"> </span><span class="n">hn</span>
<span class="w">    </span><span class="n">rcases</span><span class="w"> </span><span class="n">hn</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">pp</span><span class="o">,</span><span class="w"> </span><span class="n">p4</span><span class="o">&#10217;,</span><span class="w"> </span><span class="n">pltn</span><span class="o">&#10217;</span>
<span class="w">    </span><span class="n">exact</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">pltn</span><span class="o">,</span><span class="w"> </span><span class="n">pp</span><span class="o">,</span><span class="w"> </span><span class="n">p4</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">this</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">hs</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">h&#8321;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">((</span><span class="mi">4</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">erase</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">3</span><span class="o">)</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">exists_prime_factor_mod_4_eq_3</span><span class="w"> </span><span class="n">h&#8321;</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">pp</span><span class="o">,</span><span class="w"> </span><span class="n">pdvd</span><span class="o">,</span><span class="w"> </span><span class="n">p4eq</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">ps</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">pne3</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">erase</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">contradiction</span>
</pre></div>
</div>
<p>If you managed to complete the proof, congratulations! This has been a serious
feat of formalization.</p>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="C04_Sets_and_Functions.html" class="btn btn-neutral float-left" title="4. Sets and Functions" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="C06_Structures.html" class="btn btn-neutral float-right" title="6. Structures" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2020, Jeremy Avigad, Patrick Massot.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>