My solutions to Tao's Analysis I, formalized in Lean
danabra.mov
1import Mathlib.Tactic
2
3/-!
4# Analysis I, Appendix A.7: Equality
5
6Introduction to equality in Lean
7
8-/
9
10example : ∑' n:ℕ, 9*(10:ℝ)^(-(n:ℤ)-1) = 1 := by
11 convert_to ∑' n:ℕ, (9/10)*(1/10:ℝ)^n = 1
12 . apply tsum_congr
13 intro n
14 rw [zpow_sub₀ (by positivity), ←zpow_natCast, one_div_zpow]
15 simp; ring
16 convert_to (9/10) * ∑' n:ℕ, (1/10:ℝ)^n = 1
17 . convert tsum_const_smul'' (9/10:ℝ) (f := fun n ↦ (1/10:ℝ)^n) using 1
18 rw [tsum_geometric_of_lt_one (by norm_num) (by norm_num)]
19 norm_num
20
21example : 12 = (2:Fin 10) := by
22 decide
23
24
25/-- Reflexive axiom -/
26example {X:Type} (x:X) : x = x := by
27 rfl
28
29#check Eq.refl
30
31/-- Symmetry axiom -/
32example {X:Type} (x y:X) (h: x = y) : y = x := by
33 rw [h]
34
35#check Eq.symm
36
37/-- Transitivity axiom -/
38example {X:Type} (x y z:X) (h1: x = y) (h2: y = z) : x = z := by
39 rw [h1, h2]
40
41#check Eq.trans
42
43/-- Substitution axiom -/
44example {X Y:Type} (f:X → Y) (x y:X) (h: x = y) : f x = f y := by
45 rw [h]
46
47#check congrArg
48
49def equality_as_equiv_relation (X:Type) : Setoid X := {
50 r a b := a = b
51 iseqv := {
52 refl := Eq.refl
53 symm := Eq.symm
54 trans := Eq.trans
55 }
56}
57
58
59open Real in
60/-- Example A.7.1 -/
61example {x y:ℝ} (h:x = y) : 2*x = 2*y ∧ sin x = sin y ∧ ∀ z, x + z = y + z := by
62 and_intros
63 . rw [h]
64 . rw [h]
65 intro z
66 rw [h]
67
68/-- Example A.7.2 -/
69example {n m:ℤ} (hn: Odd n) (h: n = m) : Odd m := by
70 rw [h] at hn
71 exact hn
72
73example {n m k:ℤ} (hnk: n > k) (h: n = m) : m > k := by
74 rw [h] at hnk
75 exact hnk
76
77open Real in
78example {x y z:ℝ} (hxy : x = sin y) (hyz : y = z^2) : x = sin (z^2) := by
79 have : sin y = sin (z^2) := by rw [hyz]
80 exact hxy.trans this
81
82abbrev make_twelve_equal_two : ℤ → ℤ → Prop := fun a b ↦ a = 12 ∧ b = 2
83
84/-- A version of the integers where 12 has been forced to equal 2. -/
85abbrev NewInt := Quot make_twelve_equal_two
86
87/-- A coercion from integers to new integers -/
88instance : Coe ℤ NewInt where
89 coe n := Quot.mk make_twelve_equal_two n
90
91#check ((2:ℤ):NewInt)
92#check ((12:ℤ):NewInt)
93
94example : ((12:ℤ):NewInt) = ((2:ℤ):NewInt) := by
95 apply Quot.sound
96 simp [make_twelve_equal_two]
97
98theorem NewInt.is_coe (N:NewInt) : ∃ n:ℤ, N = (n:NewInt) := by
99 apply Quot.ind (q := N); intro n
100 use n
101
102abbrev NewInt.quot {X:Type} {f: ℤ → X} (hf: f 12 = f 2) : NewInt → X := by
103 apply Quot.lift f
104 intro a b
105 simp [make_twelve_equal_two]
106 intro ha hb
107 rw [ha, hb, hf]
108
109example {X:Type} {f:ℤ → X} (hf: f 12 = f 2) (n:ℤ) : NewInt.quot hf (n:NewInt) = f n := rfl
110
111/-- Exercise A.7.1 -/
112example {a b c d:ℝ} (hab: a = b) (hcd : c = d) : a + d = b + c := by
113 sorry