From 879abad417fb8084db85400f64429b06bbd617d9 Mon Sep 17 00:00:00 2001 From: Derrik Petrin Date: Fri, 26 Apr 2024 22:37:34 -0700 Subject: [PATCH 01/52] fix(4.1.4): grammar --- html/04_Proofs_with_Structure_II.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/html/04_Proofs_with_Structure_II.html b/html/04_Proofs_with_Structure_II.html index c886846b..ad76d76d 100644 --- a/html/04_Proofs_with_Structure_II.html +++ b/html/04_Proofs_with_Structure_II.html @@ -247,7 +247,7 @@

4.1.3. Example4.1.4. Example

Problem

-

Let \(a\) be real number whose square is at most 2, and which is greater than or equal to +

Let \(a\) be a real number whose square is at most 2, and which is greater than or equal to any real number whose square is at most 2. 1 Let \(b\) be another real number with the same two properties. Prove that \(a=b\).

From e4a62acb8c7484255ffecd89693e84a26b31da16 Mon Sep 17 00:00:00 2001 From: Derrik Petrin Date: Tue, 2 Jan 2024 22:07:04 -0800 Subject: [PATCH 02/52] fix(4.2.3): grammar --- html/04_Proofs_with_Structure_II.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/html/04_Proofs_with_Structure_II.html b/html/04_Proofs_with_Structure_II.html index ad76d76d..c2a39592 100644 --- a/html/04_Proofs_with_Structure_II.html +++ b/html/04_Proofs_with_Structure_II.html @@ -636,8 +636,8 @@

4.2.1. ExampleFirst, suppose that \(n\) is odd. Then there exists an integer \(k\) such that \(n=2k+1\). Therefore \(n-1=2k\), so \(n-1\) is divisible by 2, so \(n\equiv 1\mod 2\).

-

Conversely, suppose that \(n\equiv 1\mod 2\). Then \(2\mid n -1\), so there exists an -integer \(k\) such \(n-1=2k\). Thus \(n=2k+1\) and so \(n\) is odd.

+

Conversely, suppose that \(n\equiv 1\mod 2\). Then there exists an +integer \(k\) such that \(n-1=2k\). Thus \(n=2k+1\) and so \(n\) is odd.

We name this example Int.odd_iff_modEq for future use.

theorem odd_iff_modEq (n : ℤ) : Odd n ↔ n ≡ 1 [ZMOD 2] := by

From 885f2322b585479603ea6b612f3a2c474d08eaca Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Fri, 26 Apr 2024 22:45:35 -0700
Subject: [PATCH 03/52] fix(4.2.9): error in odd case

---
 html/04_Proofs_with_Structure_II.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/04_Proofs_with_Structure_II.html b/html/04_Proofs_with_Structure_II.html
index c2a39592..0ff5e4d5 100644
--- a/html/04_Proofs_with_Structure_II.html
+++ b/html/04_Proofs_with_Structure_II.html
@@ -824,7 +824,7 @@ 
4.2.8. ExampleLet \(n\) be an integer.  We do a case division according to the residue of \(n\)
 modulo 2.

 
If \(n\equiv 0\mod 2\), then \(n\) is even, and we are done.

-
If \(n\equiv 0\mod 2\), then \(n\) is odd, and we are done.

+
If \(n\equiv 1\mod 2\), then \(n\) is odd, and we are done.

Write this in Lean using the lemmas Int.odd_iff_modEq and Int.even_iff_modEq from Example 4.2.3 and Example 4.2.4, together with the From 747a9c72c08eb382298fe5776033cf57f1fc8f5a Mon Sep 17 00:00:00 2001 From: Derrik Petrin Date: Sun, 28 Apr 2024 22:18:26 -0700 Subject: [PATCH 04/52] fix(6.1.2): mixed up integers and nats --- html/06_Induction.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/html/06_Induction.html b/html/06_Induction.html index 5abbfc38..7ec4a646 100644 --- a/html/06_Induction.html +++ b/html/06_Induction.html @@ -220,9 +220,9 @@

6.1.2. Example\(0=2\cdot 0\).

Suppose now that for some natural number \(k\), it is true that \(k\) is either even or odd.

-

Case 1 (\(k\) is even): Then there exists an integer \(x\) such that \(k=2x\), and +

Case 1 (\(k\) is even): Then there exists a natural number \(x\) such that \(k=2x\), and so \(k+1 = 2x+1\), so \(k+1\) is odd.

-

Case 2 (\(k\) is odd): Then there exists an integer \(x\) such that \(k=2x+1\), +

Case 2 (\(k\) is odd): Then there exists a natural number \(x\) such that \(k=2x+1\), and

\[\begin{split}k+1 &= (2x+1)+1 \\ From 9134de068b12a792fea27815a8e26edb1230b2a7 Mon Sep 17 00:00:00 2001 From: Derrik Petrin Date: Sat, 6 Jan 2024 20:50:02 -0800 Subject: [PATCH 05/52] fix(6.1.5): add le 2 assumption to inductive step --- html/06_Induction.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/html/06_Induction.html b/html/06_Induction.html index 7ec4a646..ae8589ec 100644 --- a/html/06_Induction.html +++ b/html/06_Induction.html @@ -327,7 +327,7 @@

6.1.2. ExampleSolution

We prove this by induction on \(n\), starting at 2. The base case, \(3^2\geq 2^2+5\), is clear.

-

Suppose now that for some natural number \(k\), it is true that \(3 ^k\ge 2^k+5\). Then

+

Suppose now that for some natural number \(k\geq 2\), it is true that \(3 ^k\ge 2^k+5\). Then

\[\begin{split}3^{k+1} &= 2 \cdot 3^k + 3^k\\ &\ge 2(2^k+5)+3^k\\ From c17e5646376bc695cf3f3a8a8f1bc24127b87450 Mon Sep 17 00:00:00 2001 From: Derrik Petrin Date: Sun, 7 Jan 2024 15:33:20 -0800 Subject: [PATCH 06/52] fix(6.2.5): use correct multiplication dot --- html/06_Induction.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/html/06_Induction.html b/html/06_Induction.html index ae8589ec..bec9bbff 100644 --- a/html/06_Induction.html +++ b/html/06_Induction.html @@ -717,7 +717,7 @@

6.2.3. Example
\[\begin{split}0!&=1 \\ -\text{for }n:\mathbb{N},\quad(n+1)! &= (n + 1) ⬝ n!\end{split}\]
+\text{for }n:\mathbb{N},\quad(n+1)! &= (n + 1)\cdot n!\end{split}\]

def factorial : ℕ → ℕ
   | 0 => 1

From 0532915f5a081310e68b2dd73673587d56e30574 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sun, 7 Jan 2024 15:37:10 -0800
Subject: [PATCH 07/52] fix(6.2.5): use n! instead of A_n

---
 html/06_Induction.html | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/html/06_Induction.html b/html/06_Induction.html
index bec9bbff..4f0481e1 100644
--- a/html/06_Induction.html
+++ b/html/06_Induction.html
@@ -739,16 +739,16 @@ 
6.2.3. Example
 

 \[\begin{split}0!&=1 \\
-1!&=1\cdot A_0 \\
+1!&=1\cdot 0! \\
 &=1\cdot 1 \\
 &=1\\
-2!&=2\cdot A_1 \\
+2!&=2\cdot 1! \\
 &=2\cdot 1 \\
 &=2\\
-3!&=3\cdot A_2 \\
+3!&=3\cdot 2! \\
 &=3\cdot 2 \\
 &=6\\
-4!&=4\cdot A_3 \\
+4!&=4\cdot 3! \\
 &=4\cdot 6 \\
 &=24\\
 \ldots\end{split}\]


From 39252e33024a151f3f337b09d134531320a31c2d Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sat, 27 Apr 2024 20:39:10 -0700
Subject: [PATCH 08/52] fix(6.2.5): misnumbered case

---
 html/06_Induction.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/06_Induction.html b/html/06_Induction.html
index 4f0481e1..e6bedc3c 100644
--- a/html/06_Induction.html
+++ b/html/06_Induction.html
@@ -770,7 +770,7 @@ 
6.2.3. Example
 
so \(d\) is a factor of \((k+1)!\).

-
Case 1 (\(d<k+1\)): Then \(d\le k\), so by the inductive hypothesis \(d\) is a
+
Case 2 (\(d<k+1\)): Then \(d\le k\), so by the inductive hypothesis \(d\) is a
 factor of \(k!\).  Therefore there exists a natural number \(x\) such that \(k!=dx\).
 We then have

 


From 7ccd6d5e77c06a4cf51fd646de2dc2301003fc2f Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sun, 7 Jan 2024 21:28:13 -0800
Subject: [PATCH 09/52] fix(6.3.6): 6. match paper and lean statements

---
 html/06_Induction.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/06_Induction.html b/html/06_Induction.html
index e6bedc3c..65f9ec98 100644
--- a/html/06_Induction.html
+++ b/html/06_Induction.html
@@ -1340,7 +1340,7 @@ 
6.3.6. Exercises
-
Prove that for all natural numbers \(m\geq 1\), \(p_m\) is congruent to either 2 or 3
+
Prove that for all natural numbers \(m\), \(p_m\) is congruent to either 2 or 3
 modulo 7.

 
def p : ℕ → ℤ
   | 0 => 2

From 24d28a3026a71a295e6db3e50d702b71e1c0972d Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Mon, 8 Jan 2024 19:44:37 -0800
Subject: [PATCH 10/52] fix(6.4.2): use more accurate name for hypothesis

---
 Math2001/06_Induction/04_Strong_Induction.lean | 8 ++++----
 html/06_Induction.html                         | 8 ++++----
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/Math2001/06_Induction/04_Strong_Induction.lean b/Math2001/06_Induction/04_Strong_Induction.lean
index 8d68159f..ef5e8dfc 100644
--- a/Math2001/06_Induction/04_Strong_Induction.lean
+++ b/Math2001/06_Induction/04_Strong_Induction.lean
@@ -33,15 +33,15 @@ namespace Nat
 
 theorem exists_prime_factor {n : ℕ} (hn2 : 2 ≤ n) : ∃ p : ℕ, Prime p ∧ p ∣ n := by
   by_cases hn : Prime n
-  . -- case 1: `n` is prime
+  · -- case 1: `n` is prime
     use n
     constructor
     · apply hn
     · use 1
       ring
-  . -- case 2: `n` is not prime
-    obtain ⟨m, hmn, _, ⟨x, hx⟩⟩ := exists_factor_of_not_prime hn hn2
-    have IH : ∃ p, Prime p ∧ p ∣ m := exists_prime_factor hmn -- inductive hypothesis
+  · -- case 2: `n` is not prime
+    obtain ⟨m, hm2, _, ⟨x, hx⟩⟩ := exists_factor_of_not_prime hn hn2
+    have IH : ∃ p, Prime p ∧ p ∣ m := exists_prime_factor hm2 -- inductive hypothesis
     obtain ⟨p, hp, y, hy⟩ := IH
     use p
     constructor
diff --git a/html/06_Induction.html b/html/06_Induction.html
index 65f9ec98..e3a7e4fa 100644
--- a/html/06_Induction.html
+++ b/html/06_Induction.html
@@ -1490,15 +1490,15 @@ 
6.4.1. Example
 
theorem exists_prime_factor {n : ℕ} (hn2 : 2 ≤ n) : ∃ p : ℕ, Prime p ∧ p ∣ n := by
   by_cases hn : Prime n
-  . -- case 1: `n` is prime
+  · -- case 1: `n` is prime
     use n
     constructor
     · apply hn
     · use 1
       ring
-  . -- case 2: `n` is not prime
-    obtain ⟨m, hmn, _, ⟨x, hx⟩⟩ := exists_factor_of_not_prime hn hn2
-    have IH : ∃ p, Prime p ∧ p ∣ m := exists_prime_factor hmn -- inductive hypothesis
+  · -- case 2: `n` is not prime
+    obtain ⟨m, hm2, _, ⟨x, hx⟩⟩ := exists_factor_of_not_prime hn hn2
+    have IH : ∃ p, Prime p ∧ p ∣ m := exists_prime_factor hm2 -- inductive hypothesis
     obtain ⟨p, hp, y, hy⟩ := IH
     use p
     constructor

From 13f8831449a58ff8574b33dbc20e31e0718f61d6 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Tue, 9 Jan 2024 14:11:58 -0800
Subject: [PATCH 11/52] fix(6.5.3): prove correct base cases

---
 html/06_Induction.html | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/html/06_Induction.html b/html/06_Induction.html
index e3a7e4fa..8218eeb8 100644
--- a/html/06_Induction.html
+++ b/html/06_Induction.html
@@ -1702,11 +1702,11 @@ 
6.5.3. ExampleWe prove this by strong induction relative to the expression \(a+b\).

 
For all \(a\),

 

-\[\begin{split}P_{a,0}&=1\\
+\[\begin{split}P_{a,0} \ a! \ 0! &=1 \cdot a! \cdot 1\\
 &= (a+0)!,\end{split}\]

 
and for all \(b\),

 

-\[\begin{split}P_{0,b+1}&=1\\
+\[\begin{split}P_{0,b+1} \ 0! \ (b+1)! &=1 \cdot 1 \cdot (b+1)!\\
 &= (0+(b+1))!.\end{split}\]

 
Now let \(a\) and \(b\) be natural numbers and suppose that for all \(x\) and
 \(y\) with \(x+y<(a+1)+(b+1)\), it is true that \(P_{x,y} \ x! \ y! = (x+y)!\).  Then

From 5fa02ed6c6420b5c3c9566385883045e7593ffcf Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Tue, 9 Jan 2024 16:49:26 -0800
Subject: [PATCH 12/52] fix(6.6.1): nitpick: use consistent n*d order

---
 html/06_Induction.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/06_Induction.html b/html/06_Induction.html
index 8218eeb8..66a8b243 100644
--- a/html/06_Induction.html
+++ b/html/06_Induction.html
@@ -1852,7 +1852,7 @@ 
6.5.4. Exercises
Date: Tue, 9 Jan 2024 23:15:50 -0800
Subject: [PATCH 13/52] fix(6.6.2): state inductive hyp with correct vars

---
 html/06_Induction.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/06_Induction.html b/html/06_Induction.html
index 66a8b243..6b5006ed 100644
--- a/html/06_Induction.html
+++ b/html/06_Induction.html
@@ -1922,7 +1922,7 @@ 
6.5.4. ExercisesProof

 
We prove this by strong induction relative to the expression \(2n - d\).  Suppose that for all
 integers \(m\) and \(c\) with \(|2m - c|<|2n-d|\), it is true that
-\(\operatorname{mod}(n, d) + d \cdot \operatorname{div}(n, d) = n\).

+\(\operatorname{mod}(m, c) + c \cdot \operatorname{div}(m, c) = m\).

 
Case 1 (\(nd<0\)): Then by the inductive hypothesis

 

 \[\operatorname{mod}(n+d, d) + d \cdot \operatorname{div}(n+d, d) = n+d,\]


From 778230c7a04cf0ab16fc0ba8a1e7820cac2beeb0 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Thu, 2 May 2024 22:22:08 -0700
Subject: [PATCH 14/52] fix(6.6.4): case 4 of proof missing a small step

---
 html/06_Induction.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/06_Induction.html b/html/06_Induction.html
index 6b5006ed..46d004d2 100644
--- a/html/06_Induction.html
+++ b/html/06_Induction.html
@@ -2036,7 +2036,7 @@ 
6.5.4. ExercisesCase 3 (\(n=d\)): Then \(\operatorname{mod}(n, d)= 0<d\) by hypothesis.

 
Case 4 (\(0\le nd\le d^2\) and \(n\ne d\)): We have that \(n-d\le 0\), since
 \(d(n-d)\le 0\) and by hypothesis \(0<d\). Therefore \(n\le d\). Also, by hypothesis,
-\(n\ne d\).  Combining these, we have that \(n< d\).

+\(n\ne d\).  Combining these, we have that \(\operatorname{mod}(n, d)= n<d\).

 

 
theorem fmod_lt_of_pos (n : ℤ) {d : ℤ} (hd : 0 < d) : fmod n d < d := by
   rw [fmod]

From 33301ce7521afa2f89239fe891f3af9d37b47407 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Wed, 10 Jan 2024 17:53:48 -0800
Subject: [PATCH 15/52] fix(6.7.1): remove unneeded hypothesis

---
 Math2001/06_Induction/07_Euclidean_Algorithm.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Math2001/06_Induction/07_Euclidean_Algorithm.lean b/Math2001/06_Induction/07_Euclidean_Algorithm.lean
index f08e55a1..e4710048 100644
--- a/Math2001/06_Induction/07_Euclidean_Algorithm.lean
+++ b/Math2001/06_Induction/07_Euclidean_Algorithm.lean
@@ -18,7 +18,6 @@ open Int
   have H : 0 ≤ fmod a (-b)
   · apply fmod_nonneg_of_pos
     addarith [h1]
-  have h2 : 0 < -b := by addarith [h1]
   calc b < 0 := h1
     _ ≤ fmod a (-b) := H
 

From 8fac911c648c6509def52d4459f1e4a795e5fe67 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Wed, 10 Jan 2024 18:12:52 -0800
Subject: [PATCH 16/52] fix(6.7.3): state correct inductive hypothesis

---
 html/06_Induction.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/06_Induction.html b/html/06_Induction.html
index 46d004d2..7f30c7b8 100644
--- a/html/06_Induction.html
+++ b/html/06_Induction.html
@@ -2353,7 +2353,7 @@ 
6.6.6. ExercisesProof

 
We prove this by strong induction on \(b\).   Suppose that for all
 integers \(x\) and \(y\) with \(|y|<|b|\), it is true that
-\(0 \le  \operatorname{gcd}(x, y)\).

+  \(\operatorname{gcd}(x, y)\) is a factor of both \(x\) and \(y\).

 
Case 1 (\(0<b\)): Let \(q=\operatorname{div}(a,b)\) and let
 \(r=\operatorname{mod}(a,b)\), so that \(a=r+bq\) (by Example 6.6.2).

 
Then by the recursive definition \(\operatorname{gcd}(a,b)\) is equal to

From 43ad9062b804e343f2909582282b194e7fa24b17 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sat, 27 Apr 2024 21:41:11 -0700
Subject: [PATCH 17/52] fix(6.7.3): typo

---
 html/06_Induction.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/06_Induction.html b/html/06_Induction.html
index 7f30c7b8..e83d0d6f 100644
--- a/html/06_Induction.html
+++ b/html/06_Induction.html
@@ -2539,7 +2539,7 @@ 
6.6.6. Exercisestermination_by gcd_dvd_right a b => b ; gcd_dvd_left a b => b
 

 

-
There is a new tactic in the above proof: set, which introduce a short name for a long
+
There is a new tactic in the above proof: set, which introduces a short name for a long
 expression (typically one which occurs frequently and you are tired of typing out in full).  Notice
 how the goal state changes before and after its use.

 

From d61408be1de0ab4eb114a8f8d2b6fc8484623d62 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Wed, 10 Jan 2024 22:52:27 -0800
Subject: [PATCH 18/52] fix(6.7.5): state correct inductive hypothesis

---
 html/06_Induction.html | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/html/06_Induction.html b/html/06_Induction.html
index e83d0d6f..593dfac4 100644
--- a/html/06_Induction.html
+++ b/html/06_Induction.html
@@ -2663,8 +2663,9 @@ 
6.6.6. Exercises
 
Proof

 
We prove this by strong induction on \(b\).   Suppose that for all
-integers \(x\) and \(y\) with \(|y|<|b|\), it is true that
-\(0 \le  \operatorname{gcd}(x, y)\).

+integers \(x\) and \(y\) with \(|y|<|b|\), it is true that

+

+\[L(x,y)x+R(x,y)y=\operatorname{gcd}(x,y).\]

 
Case 1 (\(0<b\)): Let \(q=\operatorname{div}(a,b)\) and let
 \(r=\operatorname{mod}(a,b)\), so that \(a=r+bq\) (by Example 6.6.2).

 
Then by the recurrence definitions,


From 3eab70e7c60a3734f64029e18cdf62a8ffc4f25f Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Wed, 10 Jan 2024 23:09:57 -0800
Subject: [PATCH 19/52] fix(6.7.5): fix minus sign

---
 html/06_Induction.html | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/html/06_Induction.html b/html/06_Induction.html
index 593dfac4..bbddef83 100644
--- a/html/06_Induction.html
+++ b/html/06_Induction.html
@@ -2708,8 +2708,8 @@ 
6.6.6. Exercises\(\operatorname{gcd}(a,b)=-a\), \(L(a,b)=-1\) and \(R(a,b)=0\), so

 

 \[\begin{split}L(a,b)a+R(a,b)b
-&=-1\cdot -a+0\cdot b\\
-&=a\\
+&=-1\cdot a+0\cdot b\\
+&=-a\\
 &=\operatorname{gcd}(a,b).\end{split}\]

 

 
Here is the same proof in Lean.


From 9f838e40e59679bfee14a86923f869f5f631af46 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sun, 5 May 2024 13:05:24 -0700
Subject: [PATCH 20/52] fix(7.3): use accurate hypothesis names

---
 Math2001/07_Number_Theory/03_Sqrt_Two.lean | 4 ++--
 html/07_Number_Theory.html                 | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Math2001/07_Number_Theory/03_Sqrt_Two.lean b/Math2001/07_Number_Theory/03_Sqrt_Two.lean
index 16cc794c..68bac957 100644
--- a/Math2001/07_Number_Theory/03_Sqrt_Two.lean
+++ b/Math2001/07_Number_Theory/03_Sqrt_Two.lean
@@ -6,12 +6,12 @@ import Library.Theory.NumberTheory
 math2001_init
 
 
-@[decreasing] theorem irrat_aux_wf (b k : ℕ) (hb : k ≠ 0) (hab : b ^ 2 = 2 * k ^ 2) :
+@[decreasing] theorem irrat_aux_wf (b k : ℕ) (hk : k ≠ 0) (hbk : b ^ 2 = 2 * k ^ 2) :
     k < b := by
   have h :=
   calc k ^ 2 < k ^ 2 + k ^ 2 := by extra
     _ = 2 * k ^ 2 := by ring
-    _ = b ^ 2 := by rw [hab]
+    _ = b ^ 2 := by rw [hbk]
   cancel 2 at h
 
 
diff --git a/html/07_Number_Theory.html b/html/07_Number_Theory.html
index 8cc5c260..2e0e84ad 100644
--- a/html/07_Number_Theory.html
+++ b/html/07_Number_Theory.html
@@ -358,12 +358,12 @@
 justification for the well-foundedness of the strong induction.  Like in
 Example 6.7.1, we tag the well-foundedness lemma with
 @[decreasing] to make it available later for the strong induction.

-
@[decreasing] theorem irrat_aux_wf (b k : ℕ) (hb : k ≠ 0) (hab : b ^ 2 = 2 * k ^ 2) :
+
@[decreasing] theorem irrat_aux_wf (b k : ℕ) (hk : k ≠ 0) (hbk : b ^ 2 = 2 * k ^ 2) :
     k < b := by
   have h :=
   calc k ^ 2 < k ^ 2 + k ^ 2 := by extra
     _ = 2 * k ^ 2 := by ring
-    _ = b ^ 2 := by rw [hab]
+    _ = b ^ 2 := by rw [hbk]
   cancel 2 at h
 

 


From d79769d098134db735f1d0168e7ecefa5a1b35dc Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sun, 5 May 2024 13:05:56 -0700
Subject: [PATCH 21/52] refactor(7.3): simplify irrat_aux proof

---
 Math2001/07_Number_Theory/03_Sqrt_Two.lean | 4 +---
 html/07_Number_Theory.html                 | 4 +---
 2 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/Math2001/07_Number_Theory/03_Sqrt_Two.lean b/Math2001/07_Number_Theory/03_Sqrt_Two.lean
index 68bac957..4713abcd 100644
--- a/Math2001/07_Number_Theory/03_Sqrt_Two.lean
+++ b/Math2001/07_Number_Theory/03_Sqrt_Two.lean
@@ -34,10 +34,8 @@ theorem irrat_aux (a b : ℕ) (hb : b ≠ 0) : a ^ 2 ≠ 2 * b ^ 2 := by
       _ = k * (2 * k) := by ring
   cancel 2 * k at hk'
   have hk'' : k ≠ 0 := ne_of_gt hk'
-  have IH := irrat_aux b k -- inductive hypothesis
-  have : b ^ 2 ≠ 2 * k ^ 2 := IH hk''
+  have IH := irrat_aux b k hk'' -- inductive hypothesis
   contradiction
-termination_by _ => b
 
 
 example : ¬ ∃ a b : ℕ, b ≠ 0 ∧ a ^ 2 = 2 * b ^ 2 := by
diff --git a/html/07_Number_Theory.html b/html/07_Number_Theory.html
index 2e0e84ad..a387e879 100644
--- a/html/07_Number_Theory.html
+++ b/html/07_Number_Theory.html
@@ -388,10 +388,8 @@
       _ = k * (2 * k) := by ring
   cancel 2 * k at hk'
   have hk'' : k ≠ 0 := ne_of_gt hk'
-  have IH := irrat_aux b k -- inductive hypothesis
-  have : b ^ 2 ≠ 2 * k ^ 2 := IH hk''
+  have IH := irrat_aux b k hk'' -- inductive hypothesis
   contradiction
-termination_by _ => b
 

 

 
Finally, the main theorem is actually logically equivalent to irrat_aux, and its proof consists

From a101b73c95686b0f8aa5012250267a50af0d7efb Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sun, 5 May 2024 13:16:36 -0700
Subject: [PATCH 22/52] fix(7.3): minor typo

---
 html/07_Number_Theory.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/07_Number_Theory.html b/html/07_Number_Theory.html
index a387e879..d7fd3721 100644
--- a/html/07_Number_Theory.html
+++ b/html/07_Number_Theory.html
@@ -419,7 +419,7 @@
 \(a=dk\) and \(b=dl\).

 
Also by Example 6.7.6 (Bézout’s identity) there exist integers \(x\) and
 \(y\) such that \(xa+yb=d\).

-
The key calculation is the following  (\(\dagger\)).:

+
The key calculation is the following  (\(\dagger\)):

 

 \[\begin{split}(2k y + lx) ^ 2 \cdot d^2
   &= (2(dk) y + (d l) x) ^ 2 \\

From 53dc5c2c1dd41ccf25251c8aa1ee2b04b4e10e6a Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sun, 5 May 2024 13:06:24 -0700
Subject: [PATCH 23/52] fix(7.3): state and prove correct theorem

---
 Math2001/07_Number_Theory/03_Sqrt_Two.lean | 14 ++++++------
 html/07_Number_Theory.html                 | 26 +++++++++++-----------
 2 files changed, 20 insertions(+), 20 deletions(-)

diff --git a/Math2001/07_Number_Theory/03_Sqrt_Two.lean b/Math2001/07_Number_Theory/03_Sqrt_Two.lean
index 4713abcd..a039f746 100644
--- a/Math2001/07_Number_Theory/03_Sqrt_Two.lean
+++ b/Math2001/07_Number_Theory/03_Sqrt_Two.lean
@@ -45,7 +45,7 @@ example : ¬ ∃ a b : ℕ, b ≠ 0 ∧ a ^ 2 = 2 * b ^ 2 := by
   contradiction
 
 
-example : ¬ ∃ a b : ℤ, b ≠ 0 ∧ b ^ 2 = 2 * a ^ 2 := by
+example : ¬ ∃ a b : ℤ, b ≠ 0 ∧ a ^ 2 = 2 * b ^ 2 := by
   intro h
   obtain ⟨a, b, hb, hab⟩ := h
   have Ha : gcd a b ∣ a := gcd_dvd_left a b
@@ -55,11 +55,11 @@ example : ¬ ∃ a b : ℤ, b ≠ 0 ∧ b ^ 2 = 2 * a ^ 2 := by
   obtain ⟨x, y, h⟩ := bezout a b
   set d := gcd a b
   have key :=
-  calc (2 * k * y + l * x) ^ 2 * d ^ 2
-      = (2 * (d * k) * y + (d * l) * x) ^ 2 := by ring
-    _ = (2 * a * y + b * x) ^ 2 := by rw [hk, hl]
-    _ = 2 * (x * a + y * b) ^ 2 + (x ^ 2 - 2 * y ^ 2) * (b ^ 2 - 2 * a ^ 2) := by ring
-    _ = 2 * d ^ 2 + (x ^ 2 - 2 * y ^ 2) * (b ^ 2 - b ^ 2) := by rw [h, hab]
+  calc (2 * l * x + k * y) ^ 2 * d ^ 2
+      = (2 * (d * l) * x + (d * k) * y) ^ 2 := by ring
+    _ = (2 * b * x + a * y) ^ 2 := by rw [hk, hl]
+    _ = 2 * (x * a + y * b) ^ 2 + (y ^ 2 - 2 * x ^ 2) * (a ^ 2 - 2 * b ^ 2) := by ring
+    _ = 2 * d ^ 2 + (y ^ 2 - 2 * x ^ 2) * (a ^ 2 - a ^ 2) := by rw [h, hab]
     _ = 2 * d ^ 2 := by ring
   have hd : d ≠ 0
   · intro hd
@@ -69,5 +69,5 @@ example : ¬ ∃ a b : ℤ, b ≠ 0 ∧ b ^ 2 = 2 * a ^ 2 := by
       _ = 0 := by ring
     contradiction
   cancel d ^ 2 at key
-  have := sq_ne_two (2 * k * y + l * x)
+  have := sq_ne_two (2 * l * x + k * y)
   contradiction
diff --git a/html/07_Number_Theory.html b/html/07_Number_Theory.html
index d7fd3721..4be31d0e 100644
--- a/html/07_Number_Theory.html
+++ b/html/07_Number_Theory.html
@@ -421,11 +421,11 @@
 \(y\) such that \(xa+yb=d\).

 
The key calculation is the following  (\(\dagger\)):

 

-\[\begin{split}(2k y + lx) ^ 2 \cdot d^2
-  &= (2(dk) y + (d l) x) ^ 2 \\
-  &= (2 a y + b x) ^ 2 \\
-  &= 2  (x a + y b) ^ 2 + (x ^ 2 - 2  y ^ 2) (b ^ 2 - 2  a ^ 2) \\
-  &= 2  d ^ 2 + (x ^ 2 - 2  y ^ 2)  (b ^ 2 - b ^ 2) \\
+\[\begin{split}(2lx + ky) ^ 2 \cdot d^2
+  &= (2(dl) x + (dk) y) ^ 2 \\
+  &= (2 b x + a y) ^ 2 \\
+  &= 2 (x a + y b) ^ 2 + (y ^ 2 - 2 x ^ 2) (a ^ 2 - 2 b ^ 2) \\
+  &= 2 d ^ 2 + (y ^ 2 - 2 x ^ 2) (a ^ 2 - a ^ 2) \\
   &= 2 \cdot d^2 \\\end{split}\]

 
We have that \(d\ne 0\), since if not,

 

@@ -434,12 +434,12 @@
 &=0,\end{split}\]

 
contradiction.  Hence by (\(\dagger\)),

 

-\[(2k y + lx) ^ 2 = 2.\]

+\[(2lx + ky) ^ 2 = 2.\]

 
But by Example 2.3.5, no integer squares to 2, so this is impossible.

 

 
Note the use of Brahmagupta’s identity (Example 1.1.3) above in the middle of the key
 calculation.

-
example : ¬ ∃ a b : ℤ, b ≠ 0 ∧ b ^ 2 = 2 * a ^ 2 := by
+
example : ¬ ∃ a b : ℤ, b ≠ 0 ∧ a ^ 2 = 2 * b ^ 2 := by
   intro h
   obtain ⟨a, b, hb, hab⟩ := h
   have Ha : gcd a b ∣ a := gcd_dvd_left a b
@@ -449,11 +449,11 @@
   obtain ⟨x, y, h⟩ := bezout a b
   set d := gcd a b
   have key :=
-  calc (2 * k * y + l * x) ^ 2 * d ^ 2
-      = (2 * (d * k) * y + (d * l) * x) ^ 2 := by ring
-    _ = (2 * a * y + b * x) ^ 2 := by rw [hk, hl]
-    _ = 2 * (x * a + y * b) ^ 2 + (x ^ 2 - 2 * y ^ 2) * (b ^ 2 - 2 * a ^ 2) := by ring
-    _ = 2 * d ^ 2 + (x ^ 2 - 2 * y ^ 2) * (b ^ 2 - b ^ 2) := by rw [h, hab]
+  calc (2 * l * x + k * y) ^ 2 * d ^ 2
+      = (2 * (d * l) * x + (d * k) * y) ^ 2 := by ring
+    _ = (2 * b * x + a * y) ^ 2 := by rw [hk, hl]
+    _ = 2 * (x * a + y * b) ^ 2 + (y ^ 2 - 2 * x ^ 2) * (a ^ 2 - 2 * b ^ 2) := by ring
+    _ = 2 * d ^ 2 + (y ^ 2 - 2 * x ^ 2) * (a ^ 2 - a ^ 2) := by rw [h, hab]
     _ = 2 * d ^ 2 := by ring
   have hd : d ≠ 0
   · intro hd
@@ -463,7 +463,7 @@
       _ = 0 := by ring
     contradiction
   cancel d ^ 2 at key
-  have := sq_ne_two (2 * k * y + l * x)
+  have := sq_ne_two (2 * l * x + k * y)
   contradiction
 

 


From d213b308d85a9fe9031c1af7b42e102954645a35 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sun, 5 May 2024 21:49:52 -0700
Subject: [PATCH 24/52] fix(8.1.3): use consistent definition of `q`

---
 html/08_Functions.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/08_Functions.html b/html/08_Functions.html
index 0c9de7f8..a0da0420 100644
--- a/html/08_Functions.html
+++ b/html/08_Functions.html
@@ -220,7 +220,7 @@ 
8.1.3. Example
 
Solution

 
Let \(x_1\) and \(x_2\) be real numbers and suppose that \(q(x_1)=q(x_2)\).  Then
-\(x_1+1=x_2+1\), so \(x_1=x_2\).

+\(x_1+3=x_2+3\), so \(x_1=x_2\).

 

 
Here is this solution in Lean.  Note that after unfolding the definition “injective” using the
 command dsimp [Injective], the goal state displays


From a54bab2a61291080b489ec4e8237874d90f436ff Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sun, 19 May 2024 03:02:21 -0700
Subject: [PATCH 25/52] fix(8.1.12): reference correct exercise

---
 html/08_Functions.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/08_Functions.html b/html/08_Functions.html
index a0da0420..78910f8e 100644
--- a/html/08_Functions.html
+++ b/html/08_Functions.html
@@ -484,7 +484,7 @@ 
8.1.11. Example
 
8.1.12. Example

 
We finish with a relatively hard example.  The proof here is efficient and self-contained but not
-particularly well-motivated.  For an alternative (perhaps more intuitive) approach, combine the last
+particularly well-motivated.  For an alternative (perhaps more intuitive) approach, combine the second to last
 exercise in this section (the one about strictly monotone functions) with the idea from
 Example 2.1.8.

 


From 6a879910c43589dfcdb87df467f8e5c23fa8a3d7 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sat, 18 May 2024 16:03:51 -0700
Subject: [PATCH 26/52] fix(8.1.13): 17. real numbers -> rational numbers

---
 html/08_Functions.html | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/html/08_Functions.html b/html/08_Functions.html
index 78910f8e..01dee669 100644
--- a/html/08_Functions.html
+++ b/html/08_Functions.html
@@ -751,13 +751,13 @@ 
8.1.13. Exercises
 
 
  • Let \(f:\mathbb{Q}\to\mathbb{Q}\) be a function which is strictly monotone; that is, for
-all real numbers \(x\) and \(y\) with \(x<y\), it is true that \(f(x)<f(y)\).
+all rational numbers \(x\) and \(y\) with \(x<y\), it is true that \(f(x)<f(y)\).
 Prove that \(f\) is injective.
    
 
    You may wish to use the lemma lt_trichotomy
    
 
    lemma lt_trichotomy (x y : ℚ) : x < y ∨ x = y ∨ x < y :=
 
    
 
    
-
    which gives a case division on the relative sizes of two real numbers.
    
+
    which gives a case division on the relative sizes of two rational numbers.
    
 
    example {f : ℚ → ℚ} (hf : ∀ x y, x < y → f x < f y) : Injective f := by
   sorry
 
    

From a9785487541cd2d405338f01905032f9c6d82acf Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sat, 18 May 2024 16:04:54 -0700
Subject: [PATCH 27/52] fix(8.1.13): 17. fix lt_trichotomy statement

---
 html/08_Functions.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/08_Functions.html b/html/08_Functions.html
index 01dee669..0f0fce0e 100644
--- a/html/08_Functions.html
+++ b/html/08_Functions.html
@@ -754,7 +754,7 @@ 
    8.1.13. Exercises\(x\) and \(y\) with \(x<y\), it is true that \(f(x)<f(y)\).
 Prove that \(f\) is injective.
    
 
    You may wish to use the lemma lt_trichotomy
    
-
    lemma lt_trichotomy (x y : ℚ) : x < y ∨ x = y ∨ x < y :=
+
    lemma lt_trichotomy (x y : ℚ) : x < y ∨ x = y ∨ y < x :=
 
    
 
    
 
    which gives a case division on the relative sizes of two rational numbers.
    

From 43fdb5b1435aa81bd52e5f3926d1bf0e717152f5 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Mon, 20 May 2024 23:09:03 -0700
Subject: [PATCH 28/52] fix(8.3.1): use correct definition of `comp`

---
 html/08_Functions.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/08_Functions.html b/html/08_Functions.html
index 0f0fce0e..e79c081a 100644
--- a/html/08_Functions.html
+++ b/html/08_Functions.html
@@ -1120,7 +1120,7 @@ 
    8.3.1. DefinitionThe composition of the function \(g : Y \to Z\) with the function \(f : X \to Y\) is the
 function from \(X\) to \(Z\) which sends \(x\) to \(g(f(x))\).
    
 
    
-
    def comp (f : X → Y) (g : Y → Z) (x : X) : Z := g (f x)
+
    def comp (g : Y → Z) (f : X → Y) (x : X) : Z := g (f x)
 
    
 
    
 
    The composition of \(g : Y \to Z\) with \(f : X \to Y\) is denoted \(g \circ f\) (in

From ee3e08bf678a521ad00fe2650d865dcc5609cbad Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Tue, 21 May 2024 21:29:54 -0700
Subject: [PATCH 29/52] fix(8.3.10): 2. use rationals instead of reals

This is one option (which you've taken for most of the book, presumably
to avoid the whole noncomputable thing).

Alternatively, this could be a place to insert a footnote about the
noncomputability of division (and many other functions) over reals.

If you want to open the can of worms and mention the noncomputability,
these were a few useful links I found that discuss it:
https://leanprover.github.io/logic_and_proof/the_real_numbers.html
https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2022/Part_A/section02reals/reals.html
https://leanprover-community.github.io/archive/stream/113489-new-members/topic/function.20definition.20noncomputable.html
---
 Math2001/08_Functions/03_Composition.lean | 4 ++--
 html/08_Functions.html                    | 8 ++++----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/Math2001/08_Functions/03_Composition.lean b/Math2001/08_Functions/03_Composition.lean
index 2b38b146..17baa951 100644
--- a/Math2001/08_Functions/03_Composition.lean
+++ b/Math2001/08_Functions/03_Composition.lean
@@ -141,9 +141,9 @@ example : b ∘ a = c := by
   cases x <;> exhaust
 
 
-def u (x : ℝ) : ℝ := 5 * x + 1
+def u (x : ℚ) : ℚ := 5 * x + 1
 
-noncomputable def v (x : ℝ) : ℝ := sorry
+def v (x : ℚ) : ℚ := sorry
 
 example : Inverse u v := by
   sorry
diff --git a/html/08_Functions.html b/html/08_Functions.html
index e79c081a..27bf25b2 100644
--- a/html/08_Functions.html
+++ b/html/08_Functions.html
@@ -1412,11 +1412,11 @@ 
    8.3.10. Exercises
    
 
    
 
    • 
-
  • Consider the function \(u:\mathbb{R}\to\mathbb{R}\) defined by, \(u(x)=5x+1\). Write
-down a function \(v:\mathbb{R}\to\mathbb{R}\) which is inverse to \(u\), and prove it.
    
-
    def u (x : ℝ) : ℝ := 5 * x + 1
+
  • Consider the function \(u:\mathbb{Q}\to\mathbb{Q}\) defined by, \(u(x)=5x+1\). Write
+down a function \(v:\mathbb{Q}\to\mathbb{Q}\) which is inverse to \(u\), and prove it.
    
+
    def u (x : ℚ) : ℚ := 5 * x + 1
 
-noncomputable def v (x : ℝ) : ℝ := sorry
+def v (x : ℚ) : ℚ := sorry
 
 example : Inverse u v := by
   sorry

From c694d549de5404626f19f7400fbdd2bb230bff51 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Tue, 21 May 2024 22:16:49 -0700
Subject: [PATCH 30/52] fix(8.3.10): 5. use correct codomain for `g`

---
 html/08_Functions.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/08_Functions.html b/html/08_Functions.html
index 27bf25b2..5158d0ba 100644
--- a/html/08_Functions.html
+++ b/html/08_Functions.html
@@ -1440,7 +1440,7 @@ 
    8.3.10. Exercises
 
    • 
 
  • Let \(f : X \to Y\) be a surjective function.  Show that there exists a function
-\(g : Y \to Z\), such that \(f \circ g=\operatorname{Id}_Y\).
    
+\(g : Y \to X\), such that \(f \circ g=\operatorname{Id}_Y\).
    
 
    example {f : X → Y} (hf : Surjective f) : ∃ g : Y → X, f ∘ g = id := by
   sorry
 
    

From a509b41395957bd0d1b81d0b0ef110c778e43398 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Tue, 21 May 2024 22:37:23 -0700
Subject: [PATCH 31/52] fix(8.3.10) 7. typo

---
 html/08_Functions.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/08_Functions.html b/html/08_Functions.html
index 5158d0ba..59f355c7 100644
--- a/html/08_Functions.html
+++ b/html/08_Functions.html
@@ -1454,7 +1454,7 @@ 
    8.3.10. Exercises
 
    • 
 
  • Let \(f : X \to Y\) and \(g_1, g_2 : Y \to X\) be functions, with both \(g_1\) and
-\(g_1\) inverse to \(f\).  Show that \(g_1=g_2\).
    
+\(g_2\) inverse to \(f\).  Show that \(g_1=g_2\).
    
 
    This problem says that if a function \(f\) has an inverse, then that inverse is unique.
    
 
    example {f : X → Y} {g1 g2 : Y → X} (h1 : Inverse f g1) (h2 : Inverse f g2) :
     g1 = g2 := by

From ba285713cc7600c95d44e0c33dd9a62ff9b1ba20 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sat, 25 May 2024 17:52:38 -0700
Subject: [PATCH 32/52] fix(8.4.1): grammar

---
 html/08_Functions.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/08_Functions.html b/html/08_Functions.html
index 59f355c7..844bf314 100644
--- a/html/08_Functions.html
+++ b/html/08_Functions.html
@@ -1509,7 +1509,7 @@ 
    8.3.10. Exercises
 
    
 
    To write these proofs in Lean, notice the use of the tactic obtain in the injectivity problem to
-convert the hypothesis of a equality in a product type,
    
+convert the hypothesis of an equality in a product type,
    
 
    hm : (m1 + 1, 2 - m1) = (m2 + 1, 2 - m2)
 
    
 
    

From da8bea25fa9e46fef9ea62b9ade0a8b8f523f87e Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sat, 25 May 2024 20:19:29 -0700
Subject: [PATCH 33/52] fix(8.4.8): use correct Id function

---
 html/08_Functions.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/08_Functions.html b/html/08_Functions.html
index 844bf314..810bbb33 100644
--- a/html/08_Functions.html
+++ b/html/08_Functions.html
@@ -1835,7 +1835,7 @@ 
    8.4.8. Example
 
    Problem
    
 
    Consider the function \(g:\mathbb{R}^2\to \mathbb{R}^2\) defined by,
-\(g(x,y)=(y,x)\).  Show that \(g\circ g=\operatorname{Id}_\mathbb{R}\).
    
+\(g(x,y)=(y,x)\).  Show that \(g\circ g=\operatorname{Id}_{\mathbb{R}^2}\).
    
 
    
 
    
 
    Solution
    

From 7786e6bb5330ffad1764043d823f3c62c2d6423a Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sat, 25 May 2024 23:14:40 -0700
Subject: [PATCH 34/52] fix(8.4.9): fix the FIXME; use dsimp [i]

---
 Math2001/08_Functions/04_Product_Types.lean | 4 ++--
 html/08_Functions.html                      | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Math2001/08_Functions/04_Product_Types.lean b/Math2001/08_Functions/04_Product_Types.lean
index 9d3b04c7..43aceab9 100644
--- a/Math2001/08_Functions/04_Product_Types.lean
+++ b/Math2001/08_Functions/04_Product_Types.lean
@@ -167,14 +167,14 @@ def i : ℕ × ℕ → ℕ × ℕ
 theorem p_comp_i (x : ℕ × ℕ) : p (i x) = p x + 1 := by
   match x with
   | (0, b) =>
-    calc p (i (0, b)) = p (b + 1, 0) := by rw [i]
+    calc p (i (0, b)) = p (b + 1, 0) := by dsimp [i]
       _ = A ((b + 1) + 0) + 0 := by dsimp [p]
       _ = A (b + 1) := by ring
       _ = A b + b + 1 := by rw [A]
       _ = (A (0 + b) + b) + 1 := by ring
       _ = p (0, b) + 1 := by dsimp [p]
   | (a + 1, b) =>
-    calc p (i (a + 1, b)) = p (a, b + 1) := by rw [i] ; rfl -- FIXME
+    calc p (i (a + 1, b)) = p (a, b + 1) := by dsimp [i]
       _ = A (a + (b + 1)) + (b + 1) := by dsimp [p]
       _ = (A ((a + 1) + b) + b) + 1 := by ring
       _ = p (a + 1, b) + 1 := by rw [p]
diff --git a/html/08_Functions.html b/html/08_Functions.html
index 810bbb33..c6fd84eb 100644
--- a/html/08_Functions.html
+++ b/html/08_Functions.html
@@ -1907,14 +1907,14 @@ 
    8.4.9. Exampletheorem p_comp_i (x : ℕ × ℕ) : p (i x) = p x + 1 := by
   match x with
   | (0, b) =>
-    calc p (i (0, b)) = p (b + 1, 0) := by rw [i]
+    calc p (i (0, b)) = p (b + 1, 0) := by dsimp [i]
       _ = A ((b + 1) + 0) + 0 := by dsimp [p]
       _ = A (b + 1) := by ring
       _ = A b + b + 1 := by rw [A]
       _ = (A (0 + b) + b) + 1 := by ring
       _ = p (0, b) + 1 := by dsimp [p]
   | (a + 1, b) =>
-    calc p (i (a + 1, b)) = p (a, b + 1) := by rw [i] ; rfl -- FIXME
+    calc p (i (a + 1, b)) = p (a, b + 1) := by dsimp [i]
       _ = A (a + (b + 1)) + (b + 1) := by dsimp [p]
       _ = (A ((a + 1) + b) + b) + 1 := by ring
       _ = p (a + 1, b) + 1 := by rw [p]

From 29f0f7dc71b29e8c67cbe21e5a39deda05f01718 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sat, 25 May 2024 23:17:23 -0700
Subject: [PATCH 35/52] fix(8.4.9): prove without using zify

---
 Math2001/08_Functions/04_Product_Types.lean | 9 +++------
 html/08_Functions.html                      | 9 +++------
 2 files changed, 6 insertions(+), 12 deletions(-)

diff --git a/Math2001/08_Functions/04_Product_Types.lean b/Math2001/08_Functions/04_Product_Types.lean
index 43aceab9..e026cf06 100644
--- a/Math2001/08_Functions/04_Product_Types.lean
+++ b/Math2001/08_Functions/04_Product_Types.lean
@@ -190,13 +190,10 @@ example : Bijective p := by
       · apply of_A_add_mono
         rw [hab]
     have hb : b1 = b2
-    · zify at hab ⊢
-      calc (b1:ℤ) = A (a2 + b2) + b2 - A (a1 + b1) := by addarith [hab]
-        _ = A (a2 + b2) + b2 - A (a2 + b2) := by rw [H]
-        _ = b2 := by ring
+    · rw [H] at hab
+      addarith [hab]
     constructor
-    · zify at hb H ⊢
-      addarith [H, hb]
+    · addarith [H, hb]
     · apply hb
   · apply surjective_of_intertwining (x0 := (0, 0)) (i := i)
     · calc p (0, 0) = A (0 + 0) + 0 := by dsimp [p]
diff --git a/html/08_Functions.html b/html/08_Functions.html
index c6fd84eb..551f25ed 100644
--- a/html/08_Functions.html
+++ b/html/08_Functions.html
@@ -1930,13 +1930,10 @@ 
    8.4.9. Example· apply of_A_add_mono
         rw [hab]
     have hb : b1 = b2
-    · zify at hab ⊢
-      calc (b1:ℤ) = A (a2 + b2) + b2 - A (a1 + b1) := by addarith [hab]
-        _ = A (a2 + b2) + b2 - A (a2 + b2) := by rw [H]
-        _ = b2 := by ring
+    · rw [H] at hab
+      addarith [hab]
     constructor
-    · zify at hb H ⊢
-      addarith [H, hb]
+    · addarith [H, hb]
     · apply hb
   · apply surjective_of_intertwining (x0 := (0, 0)) (i := i)
     · calc p (0, 0) = A (0 + 0) + 0 := by dsimp [p]

From a24bd04683acb8a04766503b97a4085db60d695e Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sun, 26 May 2024 14:40:43 -0700
Subject: [PATCH 36/52] fix(8.4.10): 8. use correct Id function

---
 html/08_Functions.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/08_Functions.html b/html/08_Functions.html
index 551f25ed..8f7a8531 100644
--- a/html/08_Functions.html
+++ b/html/08_Functions.html
@@ -2011,7 +2011,7 @@ 
    8.4.10. Exercises
 
    • 
 
  • Consider the function \(h:\mathbb{R}^3\to \mathbb{R}^3\) defined by,
-\(h(x,y,z)=(y,z,x)\).  Show that \(h\circ h\circ h=\operatorname{Id}_\mathbb{R}\).
    
+\(h(x,y,z)=(y,z,x)\).  Show that \(h\circ h\circ h=\operatorname{Id}_{\mathbb{R}^3}\).
    
 
    def h : ℝ × ℝ × ℝ → ℝ × ℝ × ℝ
   | (x, y, z) => (y, z, x)
 

From 7eff382d4d7e893a8ff4802dfd81c2822c7e658d Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sun, 26 May 2024 21:43:20 -0700
Subject: [PATCH 37/52] fix(9.1.6): typo in proof

---
 html/09_Sets.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/09_Sets.html b/html/09_Sets.html
index f2f3e069..92a615ca 100644
--- a/html/09_Sets.html
+++ b/html/09_Sets.html
@@ -323,7 +323,7 @@ 
    9.1.6. Example
 
    Solution
    
 
    We will show that there exists a natural number \(x\) such that \(2\mid x\) and
-\(4\not\mid 6\).
    
+\(4\not\mid x\).
    
 
    Indeed, let us show that \(6\) has this property.  We have that \(6=2\cdot 3\), so
 \(2\mid 6\), and \(4\cdot 1 < 6 < 4 \cdot 2\), so \(4\not\mid 6\).
    
 
    

From 8e93a94ea8d9b0150adeebc10720a37750271fae Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sun, 26 May 2024 22:09:21 -0700
Subject: [PATCH 38/52] fix(9.1.8): case number typo

---
 html/09_Sets.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/09_Sets.html b/html/09_Sets.html
index 92a615ca..6839c8e6 100644
--- a/html/09_Sets.html
+++ b/html/09_Sets.html
@@ -419,7 +419,7 @@ 
    9.1.8. Example
 \[\begin{split}x^2-x-2&=(-1)^2-(-1)-2\\
 &=0.\end{split}\]
    
-
    Case 1 (\(x=2\)): Then
    
+
    Case 2 (\(x=2\)): Then
    
 
    
 \[\begin{split}x^2-x-2&=2^2-2-2\\
 &=0.\end{split}\]
    

From fab12d27152c86a2da117988f53ae43e7f4cf2bc Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sun, 26 May 2024 22:24:27 -0700
Subject: [PATCH 39/52] fix(9.1.9): typos in problem and proof

---
 html/09_Sets.html | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/html/09_Sets.html b/html/09_Sets.html
index 6839c8e6..b4b5f764 100644
--- a/html/09_Sets.html
+++ b/html/09_Sets.html
@@ -457,11 +457,11 @@ 
    9.1.8. Example9.1.9. Example
    
 
    
 
    Problem
    
-
    Prove  that \(\{1,3,6\} \subseteq\{x:\mathbb{Q} \mid t<10\}\).
    
+
    Prove  that \(\{1,3,6\} \subseteq\{t:\mathbb{Q} \mid t<10\}\).
    
 
    
 
    
 
    Solution
    
-
    We must show that for all real numbers \(t\), if \(t=1\) or \(t=3\) or \(t=6\)
+
    We must show that for all rational numbers \(t\), if \(t=1\) or \(t=3\) or \(t=6\)
 then \(t<10\).  Indeed, \(1<10\), \(3<10\) and \(6<10\).
    
 
    
 
    example : {1, 3, 6} ⊆ {t : ℚ | t < 10} := by

From 4e90bbb90d70fc720bfae281aa717bb172fadec9 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Sun, 26 May 2024 23:37:59 -0700
Subject: [PATCH 40/52] fix(9.1.10): 10. typo in proof statement

---
 html/09_Sets.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/09_Sets.html b/html/09_Sets.html
index b4b5f764..6e0c7d64 100644
--- a/html/09_Sets.html
+++ b/html/09_Sets.html
@@ -563,7 +563,7 @@ 
    9.1.10. Exercises
 
    • 
 
  • Prove or disprove that
-\(\{n:\mathbb{Z} n\mid\text{ is even}\}=\{a:\mathbb{Z} \mid a\equiv 6\mod 2\}\).
    
+\(\{n:\mathbb{Z} \mid n\text{ is even}\}=\{a:\mathbb{Z} \mid a\equiv 6\mod 2\}\).
    
 
    example : {n : ℤ | Even n} = {a : ℤ | a ≡ 6 [ZMOD 2]} := by
   sorry
 

From 99939e44a2880b828b4d8bd0eb61f9fdbf9c3546 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Mon, 27 May 2024 11:27:13 -0700
Subject: [PATCH 41/52] fix(9.2.3): use correct numeric type

---
 html/09_Sets.html | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/html/09_Sets.html b/html/09_Sets.html
index 6e0c7d64..5aafd9fe 100644
--- a/html/09_Sets.html
+++ b/html/09_Sets.html
@@ -706,9 +706,9 @@ 
    9.2.3. Example
 
    
 
    Solution
    
-
    We will show that for all real numbers \(t\), if \(t\) is -2 or 3 and \(t^2=9\) then
+
    We will show that for all rational numbers \(t\), if \(t\) is -2 or 3 and \(t^2=9\) then
 \(0<t\).
    
-
    Indeed, let \(t\) be a real number and suppose that \(t\) is -2 or 3 and \(t^2=9\).
    
+
    Indeed, let \(t\) be a rational number and suppose that \(t\) is -2 or 3 and \(t^2=9\).
    
 
    Case 1 (\(t=-2\)): We then have that
    
 
    
 \[\begin{split}(-2)^2&=t^2\\

From fc0cba57b5d30c4e70c349486e2a3c6398b1e6ce Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Mon, 27 May 2024 11:53:02 -0700
Subject: [PATCH 42/52] fix(9.2.5): use correct numeric type

---
 html/09_Sets.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/09_Sets.html b/html/09_Sets.html
index 5aafd9fe..663dece5 100644
--- a/html/09_Sets.html
+++ b/html/09_Sets.html
@@ -753,7 +753,7 @@ 
    9.2.5. Example
 
    Problem
    
 
    Show that
-\(\{n:\mathbb{Z}\mid n\text{ even}\}^{c}=\{n:\mathbb{N}\mid n\text{ odd}\}\).
    
+\(\{n:\mathbb{Z}\mid n\text{ even}\}^{c}=\{n:\mathbb{Z}\mid n\text{ odd}\}\).
    
 
    
 
    
 
    Solution
    

From 0a9216ae6f2d941e9b87cee799cdde864e2c0080 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Mon, 27 May 2024 12:20:23 -0700
Subject: [PATCH 43/52] fix(9.2.6): typos in problem statement

---
 html/09_Sets.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/09_Sets.html b/html/09_Sets.html
index 663dece5..d5726407 100644
--- a/html/09_Sets.html
+++ b/html/09_Sets.html
@@ -792,7 +792,7 @@ 
    9.2.6. Example
 
    Problem
    
 
    Show that
-\(\{n:\mathbb{Z}\mid n\equiv 1\mod 5\}\cap\{n:\mathbb{N}\mid n\equiv 1\mod 5\}=\emptyset\).
    
+\(\{n:\mathbb{Z}\mid n\equiv 1\mod 5\}\cap\{n:\mathbb{Z}\mid n\equiv 2\mod 5\}=\emptyset\).
    
 
    
 
    Let’s consider the Lean proof first.  We can write something like this:
    
 
    example : {n : ℤ | n ≡ 1 [ZMOD 5]} ∩ {n : ℤ | n ≡ 2 [ZMOD 5]} = ∅ := by

From d9cf8db6a99fa9f4d4dd2921a2cdffd667d9ec1a Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Mon, 27 May 2024 13:04:00 -0700
Subject: [PATCH 44/52] fix(9.2.8): 2. use correct problem statement

---
 html/09_Sets.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/09_Sets.html b/html/09_Sets.html
index d5726407..885fadb9 100644
--- a/html/09_Sets.html
+++ b/html/09_Sets.html
@@ -912,7 +912,7 @@ 
    9.2.8. Exercises
 
    • 
 
  • Write in an explicitly-listed finite set without repeats, or \(\emptyset\), which is equal
-to \(\{-1,2,4,4\}\cup\{3,-2,2\}\).  When you have the correct answer, the given Lean proof
+to \(\{0,1,2,3,4\}\cap\{0,2,4,6,8\}\).  When you have the correct answer, the given Lean proof
 will work.
    
 
    example : {0, 1, 2, 3, 4} ∩ {0, 2, 4, 6, 8} = sorry := by
   check_equality_of_explicit_sets

From fc8481c0a5678e8f68e43f7dbc34265f6d36848f Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Mon, 27 May 2024 13:10:16 -0700
Subject: [PATCH 45/52] fix(9.2.8): only first four use the tactic

---
 html/09_Sets.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/09_Sets.html b/html/09_Sets.html
index 885fadb9..45a3412e 100644
--- a/html/09_Sets.html
+++ b/html/09_Sets.html
@@ -897,7 +897,7 @@ 
    9.2.7. Example
 
    
 
    9.2.8. Exercises
    
-
    For the first five problems, I provide a tactic check_equality_of_explicit_sets which will prove
+
    For the first four problems, I provide a tactic check_equality_of_explicit_sets which will prove
 the statement if you have formulated it correctly.  This tactic simply runs ext, then dsimp,
 then exhaust:
    
 
    macro "check_equality_of_explicit_sets" : tactic => `(tactic| (ext; dsimp; exhaust))

From 8f1c696f6d4002b64bf96959c18d45753e4e41c1 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Wed, 29 May 2024 00:28:42 -0700
Subject: [PATCH 46/52] fix(9.3.6): 2. nitpick: consistent sequence notation

---
 html/09_Sets.html | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/html/09_Sets.html b/html/09_Sets.html
index 45a3412e..cdd7032f 100644
--- a/html/09_Sets.html
+++ b/html/09_Sets.html
@@ -1158,10 +1158,10 @@ 
    9.3.6. Exercises
    
 
    
 
    • 
-
  • Consider the sequence \(U_n\) of sets of integers defined recursively by,
    
+
  • Consider the sequence \((U_n)\) of sets of integers defined recursively by,
    
 
    
 \[\begin{split}U_0&=\mathbb{Z} \\
-\text{for }n:\mathbb{N},\quad U_{n+1} &=\{x:\mathbb{Z}\mid \exists \ y\in U_n, x = 2y \}\end{split}\]
    
+\text{for }n:\mathbb{N},\quad U_{n+1} &=\{x:\mathbb{Z}\mid \exists \ y\in U_n, x = 2y \}.\end{split}\]
    • 
 
    Show that for all natural numbers \(n\), \(U_n=\{x:\mathbb{Z}\mid 2^n\mid x\}\).
    
 
    def U : ℕ → Set ℤ
   | 0 => univ

From a3beb0dd0ac18ef3c9abb6862ffbc32206531695 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Wed, 29 May 2024 11:17:27 -0700
Subject: [PATCH 47/52] fix(10.1.1): typo in div not symm proof

---
 html/10_Relations.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/10_Relations.html b/html/10_Relations.html
index bd93d8a9..1faaccc5 100644
--- a/html/10_Relations.html
+++ b/html/10_Relations.html
@@ -153,7 +153,7 @@ 
    10.1.1. Example
 
    Solution
    
 
    We must show that there exist natural numbers \(x\) and \(y\) such that, \(x\mid y\)
-and \(y\mid x\).  Indeed, we have \(2=1\cdot 2\), so \(1\mid 2\), and
+and \(y\not \mid x\).  Indeed, we have \(2=1\cdot 2\), so \(1\mid 2\), and
 \(2\cdot 0<1<2\cdot 1\), so \(2\not \mid 1\).
    
 
    
 
    example : ¬ Symmetric ((·:ℕ) ∣ ·) := by

From 0ebacd1cf6a7214a76930d8ad84b2df9aede1fde Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Wed, 29 May 2024 11:30:29 -0700
Subject: [PATCH 48/52] fix(10.1.1): typos in proof of div antisymm

---
 html/10_Relations.html | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/html/10_Relations.html b/html/10_Relations.html
index 1faaccc5..d5d1b4fb 100644
--- a/html/10_Relations.html
+++ b/html/10_Relations.html
@@ -191,8 +191,8 @@ 
    10.1.1. Example
 
    We now return to the original problem.  We must show that for all natural numbers \(x\) and \(y\), if \(x\mid y\) and \(y\mid x\), then \(x=y\).  Indeed, let \(x\) and \(y\) be natural numbers and suppose \(x\mid y\) and \(y\mid x\). If
 \(x=0\) then by (\(\star\)) we are done; likewise if \(y=0\).  Otherwise, \(x>0\),
-so since \(y\mid x\) we have \(y\le x\), and \(y>0\),
-so since \(x\mid y\) we have \(x\le y\),  Putting these together, \(x=y\).
    
+so since \(y\mid x\) we have \(y\le x\) and \(y>0\),
+and since \(x\mid y\) we have \(x\le y\).  Putting these together, \(x=y\).
    
 
    
 
    example : AntiSymmetric ((·:ℕ) ∣ ·) := by
   have H : ∀ {m n}, m = 0 → m ∣ n → m = n

From 2ffa6d8031c074b2af155e8d66b57dc5ca0e4697 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Wed, 29 May 2024 19:45:34 -0700
Subject: [PATCH 49/52] fix(10.2.2): typo in proof

---
 html/10_Relations.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/html/10_Relations.html b/html/10_Relations.html
index d5d1b4fb..1009ea4e 100644
--- a/html/10_Relations.html
+++ b/html/10_Relations.html
@@ -686,7 +686,7 @@ 
    10.2.2. ExampleFor all integers \(x\), we have \(x^2=x^2\), so \(x\sim x\).  Therefore the relation
 \(\sim\) is reflexive.
    
 
    For all integers \(x\) and \(y\), we have that if \(x\sim y\) then \(x^2=y^2\),
-so \(y^2=x^2\), so \(y\sim z\).
+so \(y^2=x^2\), so \(y\sim x\).
 Therefore the relation \(\sim\) is symmetric.
    
 
    For all integers \(x\), \(y\) and \(z\), we have that if \(x\sim y\) and
 \(y\sim z\) then \(x^2=y^2\) and \(y^2=z^2\), so
    

From 85611b4ac8150c54266c9323990bd31d20debfc5 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Wed, 29 May 2024 20:53:10 -0700
Subject: [PATCH 50/52] fix(10.2.3): define equiv class more precisely

---
 html/10_Relations.html | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/html/10_Relations.html b/html/10_Relations.html
index 1009ea4e..b9fe6706 100644
--- a/html/10_Relations.html
+++ b/html/10_Relations.html
@@ -722,7 +722,7 @@ 
    10.2.2. Example10.2.3. Example
    
 
    You have probably guessed that the colouring can be made consistent in this way for any equivalence
 relation. Let’s make this mathematically rigorous.
    
-
    Let \(r\) be a relation on a type \(\alpha\), denoted \(\sim\) in infix notation.
    
+
    Let \(r\) be an equivalence relation on a type \(\alpha\), denoted \(\sim\) in infix notation.
    
 
    
 
    Definition
    
 
    For \(a\) in \(\alpha\), the equivalence class of \(a\) (denoted \([a]\)) is
@@ -730,7 +730,7 @@ 
    10.2.3. Example
 
    
 
    Theorem
    
-
    If the relation \(r\) is symmetric and transitive, then for all \(a_1\) and \(a_2\),
+
    Since the relation \(r\) is symmetric and transitive, for all \(a_1\) and \(a_2\),
 if \(a_1\sim a_2\), then \([a_1]=[a_2]\).
    
 
    
 
    
@@ -760,7 +760,7 @@ 
    10.2.3. Example
 
    
 
    Theorem
    
-
    If the relation \(r\) is reflexive, then every \(a\) is an element of its own equivalence
+
    Since the relation \(r\) is reflexive, every \(a\) is an element of its own equivalence
 class: \(a\in [a]\).
    
 
    
 
    

From b34ec0e121ffe8970f7cc521db06d60fe81c8784 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Thu, 30 May 2024 13:04:43 -0700
Subject: [PATCH 51/52] fix(index): fix sorting

---
 html/Index_of_Tactics.html | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/html/Index_of_Tactics.html b/html/Index_of_Tactics.html
index d43f01d8..8e800512 100644
--- a/html/Index_of_Tactics.html
+++ b/html/Index_of_Tactics.html
@@ -110,6 +110,9 @@
 
    A comparison tactic for inequalities, or other relations such as congruences: checks an inequality
 whose two sides differ by the addition of a positive quantity, a congruence mod 3 whose two sides
 differ by a multiple of 3, etc.
    
+
    have (first use: Section 2.1; with a lemma: Section 2.3; introducing a new goal: Section 2.4)
    
+
    Records a fact (followed by the proof of that fact), which then becomes available as an
+extra hypothesis.
    
 
    interval_cases (first use: Section 4.1)
    
 
    Given a natural-number or integer variable \(n\) for which numeric upper and lower bounds are
 available, produce cases for each of the numeric possibilities for \(n\).
    
@@ -119,9 +122,6 @@
 negation (\(\lnot\)) goal.
    
 
    left (first use: Section 2.3)
    
 
    Selects the left alternative of an “or” goal (\(\lor\)).
    
-
    have (first use: Section 2.1; with a lemma: Section 2.3; introducing a new goal: Section 2.4)
    
-
    Records a fact (followed by the proof of that fact), which then becomes available as an
-extra hypothesis.
    
 
    mod_cases (first use: Section 3.4)
    
 
    Introduces cases for a variable according to its residue modulo a specified number.
    
 
    * numbers (first use: Section 1.4; with at for contradictions: Section 4.4)
    

From 65a05fb5c86094f8887203e3d5438cda0e7eecb9 Mon Sep 17 00:00:00 2001
From: Derrik Petrin 
Date: Thu, 30 May 2024 13:55:23 -0700
Subject: [PATCH 52/52] fix(index): add list of missing tactics/keywords

---
 missing_tactics.md | 54 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)
 create mode 100644 missing_tactics.md

diff --git a/missing_tactics.md b/missing_tactics.md
new file mode 100644
index 00000000..18e16201
--- /dev/null
+++ b/missing_tactics.md
@@ -0,0 +1,54 @@
+- <;>
+    - first use 4.4.4
+    - for `cases` 8.1.9
+    - not sure if this is a tactic or other sort of syntax
+- by
+    - first use 1.2.1
+    -  technically a keyword for entering a mode
+- calc
+    - first use 1.2.1
+    - technically a keyword for entering a mode
+- cases
+    - first use 8.1.9
+- choose
+    - first (and only) use 8.3.7
+    - probably not necessary in index since used only in one special case
+- conv
+    - first use 5.2.1
+    - additional uses 5.2.2, 5.2.4, 9.3.4
+    - probably not worth adding to index
+- exhaust
+    - first use (finite inductive types) 8.1.8
+    - for equality proofs by set extensionality 9.2.2
+    - paired with suffices 9.2.6
+- ext:
+    - first use (function extensionality) 8.3.2
+    - syntax with product types 8.4.2
+    - with set extensionality 9.1.5
+        - special case syntax, `ext` without an argument for proof by contradiction 9.1.6
+- induction
+    - simple_induction (6.1.1)
+    - induction_from_starting_point (6.1.5)
+    - two_step_induction (6.3.1)
+    - two_step_induction_from_starting_point (6.3.5)
+- let
+    - first (and only) use 9.3.5
+    - technically a keyword
+    - probably not worth putting in index
+- match
+    - first use 6.4.1
+    - technically a keyword
+- norm_cast
+    - first use 6.5.3
+    - appears necessary to prove exercise 8 in Section 6.3, so you may want to either introduce and explain this tactic in that section, or alter the setup for that exercise to not require `norm_cast` (perhaps making `F` be type `ℕ → ℚ`?).  Or there is a way to do the proof without `norm_cast` which I was unable to figure out!
+- rfl
+    - first use 6.3.5
+    - used extensively in Chapter 8, and in 10.2.6
+- set
+    - first use 6.7.3
+    - additional uses 7.3, 10.2.5
+- split_ifs
+    - used extensively in Section 6.6 and Section 6.7
+- suffices
+    - first use 9.2.6
+    - technically a keyword