Errata chapters 6–10 plus tactics index

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

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
 

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
 
 
@@ -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
@@ -47,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
@@ -57,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
@@ -71,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

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

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]
@@ -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]

html/04_Proofs_with_Structure_II.html

@@ -247,7 +247,7 @@ <h3><span class="section-number">4.1.3. </span>Example<a class="headerlink" href
 <h3><span class="section-number">4.1.4. </span>Example<a class="headerlink" href="#id4" title="Permalink to this headline">&#61633;</a></h3>
 <div class="admonition-problem admonition">
 <p class="admonition-title">Problem</p>
-<p>Let <span class="math notranslate nohighlight">\(a\)</span> be real number whose square is at most 2, and which is greater than or equal to
+<p>Let <span class="math notranslate nohighlight">\(a\)</span> 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. <a class="footnote-reference brackets" href="#id11" id="id5">1</a> Let <span class="math notranslate nohighlight">\(b\)</span> be another real number with the same
 two properties.  Prove that <span class="math notranslate nohighlight">\(a=b\)</span>.</p>
 </div>
@@ -636,8 +636,8 @@ <h3><span class="section-number">4.2.1. </span>Example<a class="headerlink" href
 <p>First, suppose that <span class="math notranslate nohighlight">\(n\)</span> is odd.  Then there exists an integer <span class="math notranslate nohighlight">\(k\)</span> such that
 <span class="math notranslate nohighlight">\(n=2k+1\)</span>.  Therefore <span class="math notranslate nohighlight">\(n-1=2k\)</span>, so <span class="math notranslate nohighlight">\(n-1\)</span> is divisible by 2, so
 <span class="math notranslate nohighlight">\(n\equiv 1\mod 2\)</span>.</p>
-<p>Conversely, suppose that <span class="math notranslate nohighlight">\(n\equiv 1\mod 2\)</span>.  Then <span class="math notranslate nohighlight">\(2\mid n -1\)</span>, so there exists an
-integer <span class="math notranslate nohighlight">\(k\)</span> such <span class="math notranslate nohighlight">\(n-1=2k\)</span>.  Thus <span class="math notranslate nohighlight">\(n=2k+1\)</span> and so <span class="math notranslate nohighlight">\(n\)</span> is odd.</p>
+<p>Conversely, suppose that <span class="math notranslate nohighlight">\(n\equiv 1\mod 2\)</span>.  Then there exists an
+integer <span class="math notranslate nohighlight">\(k\)</span> such that <span class="math notranslate nohighlight">\(n-1=2k\)</span>.  Thus <span class="math notranslate nohighlight">\(n=2k+1\)</span> and so <span class="math notranslate nohighlight">\(n\)</span> is odd.</p>
 </div>
 <p>We name this example <code class="docutils literal notranslate"><span class="pre">Int.odd_iff_modEq</span></code> for future use.</p>
 <div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">odd_iff_modEq</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">n</span> <span class="bp">&#8596;</span> <span class="n">n</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">2</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
@@ -824,7 +824,7 @@ <h3><span class="section-number">4.2.8. </span>Example<a class="headerlink" href
 <p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer.  We do a case division according to the residue of <span class="math notranslate nohighlight">\(n\)</span>
 modulo 2.</p>
 <p>If <span class="math notranslate nohighlight">\(n\equiv 0\mod 2\)</span>, then <span class="math notranslate nohighlight">\(n\)</span> is even, and we are done.</p>
-<p>If <span class="math notranslate nohighlight">\(n\equiv 0\mod 2\)</span>, then <span class="math notranslate nohighlight">\(n\)</span> is odd, and we are done.</p>
+<p>If <span class="math notranslate nohighlight">\(n\equiv 1\mod 2\)</span>, then <span class="math notranslate nohighlight">\(n\)</span> is odd, and we are done.</p>
 </div>
 <p>Write this in Lean using the lemmas <code class="docutils literal notranslate"><span class="pre">Int.odd_iff_modEq</span></code> and <code class="docutils literal notranslate"><span class="pre">Int.even_iff_modEq</span></code> from
 <a class="reference internal" href="#odd-iff-modeq"><span class="std std-numref">Example 4.2.3</span></a> and <a class="reference internal" href="#even-iff-modeq"><span class="std std-numref">Example 4.2.4</span></a>, together with the