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\).
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
@@ -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
diff --git a/html/06_Induction.html b/html/06_Induction.html
index 5abbfc38..bbddef83 100644
--- a/html/06_Induction.html
+++ b/html/06_Induction.html
@@ -220,9 +220,9 @@
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
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
def factorial : ℕ → ℕ
| 0 => 1
@@ -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}\]
@@ -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
@@ -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
@@ -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
@@ -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
@@ -1852,7 +1852,7 @@
6.5.4. Exercises6.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,\]
@@ -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]
@@ -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
@@ -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.
@@ -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,
@@ -2707,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.
diff --git a/html/07_Number_Theory.html b/html/07_Number_Theory.html
index 8cc5c260..4be31d0e 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
@@ -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
@@ -421,13 +419,13 @@
\(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 \\
- &= (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,
@@ -436,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
@@ -451,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
@@ -465,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
diff --git a/html/08_Functions.html b/html/08_Functions.html
index 0c9de7f8..8f7a8531 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
@@ -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.
@@ -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 :=
+lemma lt_trichotomy (x y : ℚ) : x < y ∨ x = y ∨ y < x :=
-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
@@ -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))\).
-
-
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
@@ -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
@@ -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
@@ -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)
@@ -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
@@ -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]
@@ -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]
@@ -2014,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)
diff --git a/html/09_Sets.html b/html/09_Sets.html
index f2f3e069..cdd7032f 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\).
@@ -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}\]
@@ -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
@@ -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
@@ -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\\
@@ -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
@@ -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
@@ -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))
@@ -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.
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
diff --git a/html/10_Relations.html b/html/10_Relations.html
index bd93d8a9..b9fe6706 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
@@ -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
@@ -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
@@ -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]\).
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)
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