Merge pull request #240 from teorth:Comment-2.3

add comments to Sec 2.3

Author: teorth

analysis/Analysis/Section_2_3.lean

@@ -32,37 +32,45 @@ abbrev Nat.mul (n m : Nat) : Nat := Nat.recurse (fun _ prod ↦ prod + m) 0 n
 instance Nat.instMul : Mul Nat where
   mul := mul
 
-/-- Definition 2.3.1 (Multiplication of natural numbers) -/
+/-- Definition 2.3.1 (Multiplication of natural numbers)
+Compare with Mathlib's `Nat.zero_mul` -/
 theorem Nat.zero_mul (m: Nat) : 0 * m = 0 := recurse_zero (fun _ prod ↦ prod+m) _
 
-/-- Definition 2.3.1 (Multiplication of natural numbers) -/
+/-- Definition 2.3.1 (Multiplication of natural numbers)
+Compare with Mathlib's `Nat.succ_mul` -/
 theorem Nat.succ_mul (n m: Nat) : (n++) * m = n * m + m := recurse_succ (fun _ prod ↦ prod+m) _ _
 
 theorem Nat.one_mul' (m: Nat) : 1 * m = 0 + m := by
   rw [←zero_succ, succ_mul, zero_mul]
 
+/-- Compare with Mathlib's `Nat.one_mul` -/
 theorem Nat.one_mul (m: Nat) : 1 * m = m := by
   rw [one_mul', zero_add]
 
 theorem Nat.two_mul (m: Nat) : 2 * m = 0 + m + m := by
   rw [←one_succ, succ_mul, one_mul']
 
-/-- This lemma will be useful to prove Lemma 2.3.2. -/
+/-- This lemma will be useful to prove Lemma 2.3.2.
+Compare with Mathlib's `Nat.mul_zero` -/
 lemma Nat.mul_zero (n: Nat) : n * 0 = 0 := by
   sorry
 
-/-- This lemma will be useful to prove Lemma 2.3.2. -/
+/-- This lemma will be useful to prove Lemma 2.3.2.
+Compare with Mathlib's `Nat.mul_succ` -/
 lemma Nat.mul_succ (n m:Nat) : n * m++ = n * m + n := by
   sorry
 
-/-- Lemma 2.3.2 (Multiplication is commutative) / Exercise 2.3.1 -/
+/-- Lemma 2.3.2 (Multiplication is commutative) / Exercise 2.3.1
+Compare with Mathlib's `Nat.mul_comm` -/
 lemma Nat.mul_comm (n m: Nat) : n * m = m * n := by
   sorry
 
+/-- Compare with Mathlib's `Nat.mul_one` -/
 theorem Nat.mul_one (m: Nat) : m * 1 = m := by
   rw [mul_comm, one_mul]
 
-/-- This lemma will be useful to prove Lemma 2.3.3. -/
+/-- This lemma will be useful to prove Lemma 2.3.3.
+Compare with Mathlib's `Nat.mul_pos` -/
 lemma Nat.pos_mul_pos {n m: Nat} (h₁: n.IsPos) (h₂: m.IsPos) : (n * m).IsPos := by
   sorry
 
@@ -71,7 +79,8 @@ lemma Nat.pos_mul_pos {n m: Nat} (h₁: n.IsPos) (h₂: m.IsPos) : (n * m).IsPos
 lemma Nat.mul_eq_zero (n m: Nat) : n * m = 0 ↔ n = 0 ∨ m = 0 := by
   sorry
 
-/-- Proposition 2.3.4 (Distributive law)-/
+/-- Proposition 2.3.4 (Distributive law)
+Compare with Mathlib's `Nat.mul_add` -/
 theorem Nat.mul_add (a b c: Nat) : a * (b + c) = a * b + a * c := by
   -- This proof is written to follow the structure of the original text.
   revert c; apply induction
@@ -81,11 +90,13 @@ theorem Nat.mul_add (a b c: Nat) : a * (b + c) = a * b + a * c := by
   rw [add_succ, mul_succ]
   rw [mul_succ, ←add_assoc, ←habc]
 
-/-- Proposition 2.3.4 (Distributive law)-/
+/-- Proposition 2.3.4 (Distributive law)
+Compare with Mathlib's `Nat.add_mul`  -/
 theorem Nat.add_mul (a b c: Nat) : (a + b)*c = a*c + b*c := by
   simp only [mul_comm, mul_add]
 
-/-- Proposition 2.3.5 (Multiplication is associative) / Exercise 2.3.3 -/
+/-- Proposition 2.3.5 (Multiplication is associative) / Exercise 2.3.3
+Compare with Mathlib's `Nat.mul_assoc` -/
 theorem Nat.mul_assoc (a b c: Nat) : (a * b) * c = a * (b * c) := by
   sorry
 
@@ -106,7 +117,8 @@ instance Nat.instCommSemiring : CommSemiring Nat where
 example (a b c d:ℕ) : (a+b)*1*(c+d) = d*b+a*c+c*b+a*d+0 := by ring
 
 
-/-- Proposition 2.3.6 (Multiplication preserves order) -/
+/-- Proposition 2.3.6 (Multiplication preserves order)
+Compare with Mathlib's `Nat.mul_lt_mul_of_pos_right` -/
 theorem Nat.mul_lt_mul_of_pos_right {a b c: Nat} (h: a < b) (hc: c.IsPos) : a * c < b * c := by
   -- This proof is written to follow the structure of the original text.
   rw [lt_iff_add_pos] at h
@@ -121,7 +133,8 @@ theorem Nat.mul_lt_mul_of_pos_right {a b c: Nat} (h: a < b) (hc: c.IsPos) : a *
 theorem Nat.mul_gt_mul_of_pos_right {a b c: Nat} (h: a > b) (hc: c.IsPos) :
     a * c > b * c := mul_lt_mul_of_pos_right h hc
 
-/-- Proposition 2.3.6 (Multiplication preserves order) -/
+/-- Proposition 2.3.6 (Multiplication preserves order)
+Compare with Mathlib's `Nat.mul_lt_mul_of_pos_left` -/
 theorem Nat.mul_lt_mul_of_pos_left {a b c: Nat} (h: a < b) (hc: c.IsPos) : c * a < c * b := by
   simp [mul_comm]
   exact mul_lt_mul_of_pos_right h hc
@@ -130,7 +143,8 @@ theorem Nat.mul_lt_mul_of_pos_left {a b c: Nat} (h: a < b) (hc: c.IsPos) : c * a
 theorem Nat.mul_gt_mul_of_pos_left {a b c: Nat} (h: a > b) (hc: c.IsPos) :
     c * a > c * b := mul_lt_mul_of_pos_left h hc
 
-/-- Corollary 2.3.7 (Cancellation law) -/
+/-- Corollary 2.3.7 (Cancellation law)
+Compare with Mathlib's `Nat.mul_right_cancel` -/
 lemma Nat.mul_cancel_right {a b c: Nat} (h: a * c = b * c) (hc: c.IsPos) : a = b := by
   -- This proof is written to follow the structure of the original text.
   have := trichotomous a b
@@ -143,18 +157,22 @@ lemma Nat.mul_cancel_right {a b c: Nat} (h: a * c = b * c) (hc: c.IsPos) : a = b
   replace hgt := ne_of_gt _ _ hgt
   contradiction
 
-/-- (Not from textbook) Nat is an ordered semiring. -/
+/-- (Not from textbook) Nat is an ordered semiring.
+This allows tactics such as `gcongr` to apply to the Chapter 2 natural numbers. -/
 instance Nat.isOrderedRing : IsOrderedRing Nat where
   zero_le_one := by sorry
   mul_le_mul_of_nonneg_left := by sorry
   mul_le_mul_of_nonneg_right := by sorry
 
+/-- This illustration of the `gcongr` tactic is not from the
+    textbook. -/
 example (a b c d:Nat) (hab: a ≤ b) : c*a*d ≤ c*b*d := by
   gcongr
   . exact d.zero_le
   exact c.zero_le
 
-/-- Proposition 2.3.9 (Euclid's division lemma) / Exercise 2.3.5 -/
+/-- Proposition 2.3.9 (Euclid's division lemma) / Exercise 2.3.5
+Compare with Mathlib's `Nat.mod_eq_iff` -/
 theorem Nat.exists_div_mod (n:Nat) {q: Nat} (hq: q.IsPos) :
     ∃ m r: Nat, 0 ≤ r ∧ r < q ∧ n = m * q + r := by
   sorry
@@ -165,16 +183,25 @@ abbrev Nat.pow (m n: Nat) : Nat := Nat.recurse (fun _ prod ↦ prod * m) 1 n
 instance Nat.instPow : HomogeneousPow Nat where
   pow := Nat.pow
 
-/-- Definition 2.3.11 (Exponentiation for natural numbers) -/
+/-- Definition 2.3.11 (Exponentiation for natural numbers)
+Compare with Mathlib's `Nat.pow_zero` -/
+@[simp]
 theorem Nat.pow_zero (m: Nat) : m ^ (0:Nat) = 1 := recurse_zero (fun _ prod ↦ prod * m) _
 
 /-- Definition 2.3.11 (Exponentiation for natural numbers) -/
+@[simp]
 theorem Nat.zero_pow_zero : (0:Nat) ^ 0 = 1 := recurse_zero (fun _ prod ↦ prod * 0) _
 
-/-- Definition 2.3.11 (Exponentiation for natural numbers) -/
+/-- Definition 2.3.11 (Exponentiation for natural numbers)
+Compare with Mathlib's `Nat.pow_succ` -/
 theorem Nat.pow_succ (m n: Nat) : (m:Nat) ^ n++ = m^n * m :=
   recurse_succ (fun _ prod ↦ prod * m) _ _
 
+/-- Compare with Mathlib's `Nat.pow_one` -/
+@[simp]
+theorem Nat.pow_one (m: Nat) : m ^ (1:Nat) = m := by
+  rw [←zero_succ, pow_succ]; simp
+
 /-- Exercise 2.3.4-/
 theorem Nat.sq_add_eq (a b: Nat) :
     (a + b) ^ (2 : Nat) = a ^ (2 : Nat) + 2 * a * b + b ^ (2 : Nat) := by

analysis/Analysis/Section_3_6.lean

@@ -103,7 +103,7 @@ theorem SetTheory.Set.card_erase {n:ℕ} (h: n ≥ 1) {X:Set} (hX: X.has_card n)
         have := SetTheory.Set.Fin.toNat_lt (f (ι x'))
         have : (f (ι x'):ℕ) ≠ m₀ := by
           have := x'.property
-          simp [X'] at this; contrapose! this; intro hx'; simp [←this, Subtype.val_inj] at hm₀f
+          simp [X'] at this; contrapose! this; intros; simp [←this, Subtype.val_inj] at hm₀f
           exact (congrArg Subtype.val (hf.1 hm₀f)).symm
         omega)
   have hg_def (x':X') : if (f (ι x'):ℕ) < m₀ then (g x':ℕ) = f (ι x') else (g x':ℕ) = f (ι x') - 1 := by