Update to v4.8.0

Appendix.qmd

@@ -196,7 +196,7 @@ There is a `show` tactic in standard Lean, but it works a little differently fro
 | `⋃₀` | `\U0` |
 | `⋂₀` | `\I0` |
 | `\` | `\\` |
-| `△` | `\bigtriangleup` |
+| `∆` | `\symmdiff` |
 | `∅` | `\emptyset` |
 | `𝒫` | `\powerset` |
 | `·` | `\.` |

Chap3.qmd

@@ -496,7 +496,7 @@ You may plug in any value of type `U`, say `a`, for `x` and use this given to co
 
 This strategy says that if you have `h : ∀ (x : U), P x` and `a : U`, then you can infer `P a`.  Indeed, in this situation Lean will recognize `h a` as a proof of `P a`.  For example, you can write `have h' : P a := h a` in a Lean tactic-mode proof, and Lean will add `h' : P a` to the tactic state.  Note that `a` here need not be simply a variable; it can be any expression denoting an object of type `U`.
 
-Let's try these strategies out in a Lean proof.  In Lean, if you don't want to give a theorem a name, you can simply call it an `example` rather than a `theorem`, and then there is no need to give it a name.  In the following theorem, you can enter the symbol `∀` by typing `\forall` or `\all`, and you can enter `∃` by typing `\exists` or `\ex`.
+Let's try these strategies out in a Lean proof.  In Lean, if you don't want to give a theorem a name, you can simply call it an `example` rather than a `theorem`, and then there is no need to give it a name.  In the following example, you can enter the symbol `∀` by typing `\forall` or `\all`, and you can enter `∃` by typing `\exists` or `\ex`.
 
 ::: {.inout}
 ::: {.inpt}
@@ -657,7 +657,7 @@ Our next example is a theorem of set theory.  You already know how to type a few
 | `∪` | `\union` or `\cup` |
 | `∩` | `\inter` or `\cap` |
 | `\` | `\\` |
-| `△` | `\bigtriangleup` |
+| `∆` | `\symmdiff` |
 | `∅` | `\emptyset` |
 | `𝒫` | `\powerset` |
 :::
@@ -3135,7 +3135,7 @@ theorem Exercise_3_5_18 (U : Type) (F G H : Set (Set U))
 ::: {.numex arguments="7"}
 ```lean
 theorem Exercise_3_5_24a (U : Type) (A B C : Set U) :
-    (A ∪ B) △ C ⊆ (A △ C) ∪ (B △ C) := sorry
+    (A ∪ B) ∆ C ⊆ (A ∆ C) ∪ (B ∆ C) := sorry
 ```
 :::
 
@@ -4007,15 +4007,15 @@ theorem union_comm {U : Type} (X Y : Set U) :
   done
 ```
 
-It takes a few seconds for Lean to search its library of theorems, but eventually a blue squiggle appears under `apply?`, indicating that the tactic has produced an answer.  You will find the answer in the Infoview pane:  `Try this: exact or_comm`.  The word `exact` is the name of a tactic that we have not discussed; it is a shorthand for `show _ from`, where the blank gets filled in with the goal.  Thus, you can think of `apply?`'s answer as a shortened form of the tactic
+It takes a few seconds for Lean to search its library of theorems, but eventually a blue squiggle appears under `apply?`, indicating that the tactic has produced an answer.  You will find the answer in the Infoview pane:  `Try this: exact Or.comm`.  The word `exact` is the name of a tactic that we have not discussed; it is a shorthand for `show _ from`, where the blank gets filled in with the goal.  Thus, you can think of `apply?`'s answer as a shortened form of the tactic
 
 ::: {.ind}
 ```
-show x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∨ x ∈ X from or_comm
+show x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∨ x ∈ X from Or.comm
 ```
 :::
 
-Of course, this is precisely the step we used earlier to complete the proof.
+The command `#check @Or.comm` will tell you that `Or.comm` is just an alternative name for the theorem `or_comm`.  So the step suggested by the `apply?` tactic is essentially the same as the step we used earlier to complete the proof.
 
 Usually your proof will be more readable if you use the `show` tactic to state explicitly the goal that is being proven.  This also gives Lean a chance to correct you if you have become confused about what goal you are proving.  But sometimes---for example, if the goal is very long---it is convenient to use the `exact` tactic instead.  You might think of `exact` as meaning "the following is a term-mode proof that is exactly what is needed to prove the goal."
 
@@ -4039,6 +4039,7 @@ theorem Exercise_3_5_9 (U : Type) (A B : Set U)
     (h1 : 𝒫 (A ∪ B) = 𝒫 A ∪ 𝒫 B) : A ⊆ B ∨ B ⊆ A := by
   --Hint:  Start like this:
   have h2 : A ∪ B ∈ 𝒫 (A ∪ B) := sorry
+  
   **done::
 ```
 :::

Chap6.qmd

@@ -890,7 +890,7 @@ How can we prove `2 ^ n > 0`?  It is often helpful to think about whether there
 example (m n : Nat) (h : m > 0) : m ^ n > 0 := by ++apply?::
 ```
 
-The `apply?` tactic comes up with `exact Nat.pos_pow_of_pos n h`, and `#check @pos_pow_of_pos` gives the result
+The `apply?` tactic comes up with `exact Nat.pos_pow_of_pos n h`, and `#check @Nat.pos_pow_of_pos` gives the result
 
 ::: {.ind}
 ```
@@ -947,7 +947,7 @@ theorem Example_6_3_1 : ∀ n ≥ 4, fact n > 2 ^ n := by
   done
 ```
 
-The next example in *HTPI* is a proof of one of the laws of exponents:  `a ^ (m + n) = a ^ m * a ^ n`.  Lean's definition of exponentiation with natural number exponents is recursive.  For some reason, the definitions are slightly different for different kinds of bases.  The definitions Lean uses are essentially as follows:
+The next example in *HTPI* is a proof of one of the laws of exponents:  `a ^ (m + n) = a ^ m * a ^ n`.  Lean's definition of exponentiation with natural number exponents is recursive.  The definitions Lean uses are essentially as follows:
 
 ```lean
 --For natural numbers b and k, b ^ k = nat_pow b k:
@@ -960,7 +960,7 @@ def nat_pow (b k : Nat) : Nat :=
 def real_pow (b : Real) (k : Nat) : Real :=
   match k with
     | 0 => 1
-    | n + 1 => b * (real_pow b n)
+    | n + 1 => (real_pow b n) * b
 ```
 
 Let's prove the addition law for exponents:
@@ -994,10 +994,9 @@ theorem Example_6_3_2 : ∀ (a : Real) (m n : Nat),
     show a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1) from
       calc a ^ (m + (n + 1))
         _ = a ^ ((m + n) + 1) := by rw [add_assoc]
-        _ = a * a ^ (m + n) := by rfl
-        _ = a * (a ^ m * a ^ n) := by rw [ih]
-        _ = a ^ m * (a * a ^ n) := by
-              rw [←mul_assoc, mul_comm a, mul_assoc]
+        _ = a ^ (m + n) * a := by rfl
+        _ = (a ^ m * a ^ n) * a := by rw [ih]
+        _ = a ^ m * (a ^ n * a) := by rw [mul_assoc]
         _ = a ^ m * (a ^ (n + 1)) := by rfl
     done
   done
@@ -1116,10 +1115,10 @@ theorem ??Example_6_3_4:: : ∀ (x : Real), x > -1 →
     rewrite [Nat.cast_succ]
     show (1 + x) ^ (n + 1) ≥ 1 + (n + 1) * x from
       calc (1 + x) ^ (n + 1)
-        _ = (1 + x) * (1 + x) ^ n := by rfl
-        _ ≥ (1 + x) * (1 + n * x) := sorry
-        _ = 1 + x + n * x + n * x ^ 2 := by ring
-        _ ≥ 1 + x + n * x + 0 := sorry
+        _ = (1 + x) ^ n * (1 + x) := by rfl
+        _ ≥ (1 + n * x) * (1 + x) := sorry
+        _ = 1 + n * x + x + n * x ^ 2 := by ring
+        _ ≥ 1 + n * x + x + 0 := sorry
         _ = 1 + (n + 1) * x := by ring
     done
   done
@@ -1146,10 +1145,10 @@ theorem ??Example_6_3_4:: : ∀ (x : Real), x > -1 →
     have h2 : 0 ≤ 1 + x := by linarith
     show (1 + x) ^ (n + 1) ≥ 1 + (n + 1) * x from
       calc (1 + x) ^ (n + 1)
-        _ = (1 + x) * (1 + x) ^ n := by rfl
-        _ ≥ (1 + x) * (1 + n * x) := by rel [ih]
-        _ = 1 + x + n * x + n * x ^ 2 := by ring
-        _ ≥ 1 + x + n * x + 0 := sorry
+        _ = (1 + x) ^ n * (1 + x) := by rfl
+        _ ≥ (1 + n * x) * (1 + x) := by rel [ih]
+        _ = 1 + n * x + x + n * x ^ 2 := by ring
+        _ ≥ 1 + n * x + x + 0 := sorry
         _ = 1 + (n + 1) * x := by ring
     done
   done
@@ -1159,8 +1158,9 @@ For the second `sorry` step, we'll need to know that `n * x ^ 2 ≥ 0`.  To prov
 
 ::: {.ind}
 ```
-@sq_nonneg : ∀ {R : Type u_1} [inst : LinearOrderedRing R]
-              (a : R), 0 ≤ a ^ 2
+@sq_nonneg : ∀ {α : Type u_1} [inst : LinearOrderedSemiring α]
+              [inst_1 : ExistsAddOfLE α]
+              (a : α), 0 ≤ a ^ 2
 ```
 :::
 
@@ -1188,10 +1188,10 @@ theorem Example_6_3_4 : ∀ (x : Real), x > -1 →
         _ = 0 := by ring
     show (1 + x) ^ (n + 1) ≥ 1 + (n + 1) * x from
       calc (1 + x) ^ (n + 1)
-        _ = (1 + x) * (1 + x) ^ n := by rfl
-        _ ≥ (1 + x) * (1 + n * x) := by rel [ih]
-        _ = 1 + x + n * x + n * x ^ 2 := by ring
-        _ ≥ 1 + x + n * x + 0 := by rel [h4]
+        _ = (1 + x) ^ n * (1 + x) := by rfl
+        _ ≥ (1 + n * x) * (1 + x) := by rel [ih]
+        _ = 1 + n * x + x + n * x ^ 2 := by ring
+        _ ≥ 1 + n * x + x + 0 := by rel [h4]
         _ = 1 + (n + 1) * x := by ring
     done
   done
@@ -1509,7 +1509,7 @@ theorem well_ord_princ (S : Set Nat) : (∃ (n : Nat), n ∈ S) →
   done
 ```
 
-Section 6.4 of *HTPI* ends with an example of an application of the well ordering principle.  The example gives a proof that $\sqrt{2}$ is irrational.  If $\sqrt{2}$ were rational, then there would be natural numbers $p$ and $q$ such that $q \ne 0$ and $p/q = \sqrt{2}$, and therefore $p^2 = 2q^2$.  So we can prove that $\sqrt{2}$ is irrational by showing that there do not exist natural numbers $p$ and $q$ such that $q \ne 0$ and $p^2 = 2q^2$.
+Section 6.4 of *HTPI* ends with an example of an application of the well-ordering principle.  The example gives a proof that $\sqrt{2}$ is irrational.  If $\sqrt{2}$ were rational, then there would be natural numbers $p$ and $q$ such that $q \ne 0$ and $p/q = \sqrt{2}$, and therefore $p^2 = 2q^2$.  So we can prove that $\sqrt{2}$ is irrational by showing that there do not exist natural numbers $p$ and $q$ such that $q \ne 0$ and $p^2 = 2q^2$.
 
 The proof uses a definition from the exercises of Section 6.1:
 
@@ -1529,7 +1529,7 @@ And we'll need another theorem that we haven't seen before:
 ```
 @mul_left_cancel_iff_of_pos : ∀ {α : Type u_1} {a b c : α}
                     [inst : MulZeroClass α] [inst_1 : PartialOrder α]
-                    [inst_2 : PosMulMonoRev α],
+                    [inst_2 : PosMulReflectLE α],
                     0 < a → (a * b = a * c ↔ b = c)
 ```
 :::
@@ -1549,7 +1549,7 @@ S = {q : Nat | ∃ (p : Nat), p * p = 2 * (q * q) ∧ q ≠ 0}
 ```
 :::
 
-would be nonempty, and therefore, by the well ordering principle, it would have a smallest element.  We then show that this leads to a contradiction.  Here is the proof.
+would be nonempty, and therefore, by the well-ordering principle, it would have a smallest element.  We then show that this leads to a contradiction.  Here is the proof.
 
 ```lean
 theorem Theorem_6_4_5 :