Analysis I, Appendix A.7: Equality

Introduction to equality in Lean

example : ∑' n:ℕ, 9*(10:ℝ)^(-(n:ℤ)-1) = 1 := by⊢ ∑' (n : ℕ), 9 * 10 ^ (-↑n - 1) = 1
  convert_to ∑' n:ℕ, (9/10)*(1/10:ℝ)^n = 1h.e'_2⊢ ∑' (n : ℕ), 9 * 10 ^ (-↑n - 1) = ∑' (n : ℕ), 9 / 10 * (1 / 10) ^ n⊢ ∑' (n : ℕ), 9 / 10 * (1 / 10) ^ n = 1
  .h.e'_2⊢ ∑' (n : ℕ), 9 * 10 ^ (-↑n - 1) = ∑' (n : ℕ), 9 / 10 * (1 / 10) ^ n apply tsum_congrh.e'_2.hfg⊢ ∀ (b : ℕ), 9 * 10 ^ (-↑b - 1) = 9 / 10 * (1 / 10) ^ b
    intro nh.e'_2.hfgn:ℕ⊢ 9 * 10 ^ (-↑n - 1) = 9 / 10 * (1 / 10) ^ n
    rw [zpow_sub₀ (by positivity), ←zpow_natCast, one_div_zpow]h.e'_2.hfgn:ℕ⊢ 9 * (10 ^ (-↑n) / 10 ^ 1) = 9 / 10 * (1 / 10 ^ ↑n)
    simph.e'_2.hfgn:ℕ⊢ 9 * ((10 ^ n)⁻¹ / 10) = 9 / 10 * (10 ^ n)⁻¹; ringAll goals completed! 🐙
  convert_to (9/10) * ∑' n:ℕ, (1/10:ℝ)^n = 1h.e'_2⊢ ∑' (n : ℕ), 9 / 10 * (1 / 10) ^ n = 9 / 10 * ∑' (n : ℕ), (1 / 10) ^ n⊢ 9 / 10 * ∑' (n : ℕ), (1 / 10) ^ n = 1
  .h.e'_2⊢ ∑' (n : ℕ), 9 / 10 * (1 / 10) ^ n = 9 / 10 * ∑' (n : ℕ), (1 / 10) ^ n convert tsum_const_smul'' (9/10:ℝ) (f := fun n ↦ (1/10:ℝ)^n) using 1All goals completed! 🐙
  rw [tsum_geometric_of_lt_one (by norm_num) (by norm_num)]⊢ 9 / 10 * (1 - 1 / 10)⁻¹ = 1
  norm_numAll goals completed! 🐙

example : 12 = (2:Fin 10)  := by⊢ 12 = 2
  decideAll goals completed! 🐙

/-- Reflexive axiom -/
example {X:Type} (x:X) : x = x := byX:Typex:X⊢ x = x
  rflAll goals completed! 🐙

Eq.refl.{u_1} {α : Sort u_1} (a : α) : a = a#check Eq.refl

Eq.refl.{u_1} {α : Sort u_1} (a : α) : a = a

/-- Symmetry axiom -/
example {X:Type} (x y:X) (h: x = y) : y = x := byX:Typex:Xy:Xh:x = y⊢ y = x
  rw [h]All goals completed! 🐙

Eq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a#check Eq.symm

Eq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a

/-- Transitivity axiom -/
example {X:Type} (x y z:X) (h1: x = y) (h2: y = z) : x = z := byX:Typex:Xy:Xz:Xh1:x = yh2:y = z⊢ x = z
  rw [h1, h2]All goals completed! 🐙

Eq.trans.{u} {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c#check Eq.trans

Eq.trans.{u} {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c

/-- Substitution axiom -/
example {X Y:Type} (f:X → Y) (x y:X) (h: x = y) : f x = f y := byX:TypeY:Typef:X → Yx:Xy:Xh:x = y⊢ f x = f y
  rw [h]All goals completed! 🐙

congrArg.{u, v} {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂#check congrArg

congrArg.{u, v} {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂

def equality_as_equiv_relation (X:Type) : Setoid X := {
  r a b := a = b
  iseqv := {
    refl := Eq.refl
    symm := Eq.symm
    trans := Eq.trans
  }
}

open Real in
/-- Example A.7.1 -/
example {x y:ℝ} (h:x = y) : 2*x = 2*y ∧ sin x = sin y ∧ ∀ z, x + z = y + z := byx:ℝy:ℝh:x = y⊢ 2 * x = 2 * y ∧ sin x = sin y ∧ ∀ (z : ℝ), x + z = y + z
  split_andsrefine_1x:ℝy:ℝh:x = y⊢ 2 * x = 2 * yrefine_2.refine_1x:ℝy:ℝh:x = y⊢ sin x = sin yrefine_2.refine_2x:ℝy:ℝh:x = y⊢ ∀ (z : ℝ), x + z = y + z
  .refine_1x:ℝy:ℝh:x = y⊢ 2 * x = 2 * y rw [h]All goals completed! 🐙
  .refine_2.refine_1x:ℝy:ℝh:x = y⊢ sin x = sin y rw [h]All goals completed! 🐙
  intro zrefine_2.refine_2x:ℝy:ℝh:x = yz:ℝ⊢ x + z = y + z
  rw [h]All goals completed! 🐙

/-- Example A.7.2 -/
example {n m:ℤ} (hn: Odd n) (h: n = m) : Odd m := byn:ℤm:ℤhn:Odd nh:n = m⊢ Odd m
  rw [h] at hnn:ℤm:ℤhn:Odd mh:n = m⊢ Odd m
  exact hnAll goals completed! 🐙

example {n m k:ℤ} (hnk: n > k) (h: n = m) : m > k := byn:ℤm:ℤk:ℤhnk:n > kh:n = m⊢ m > k
  rw [h] at hnkn:ℤm:ℤk:ℤhnk:m > kh:n = m⊢ m > k
  exact hnkAll goals completed! 🐙

open Real in
example {x y z:ℝ} (hxy : x = sin y) (hyz : y = z^2) : x = sin (z^2) := byx:ℝy:ℝz:ℝhxy:x = sin yhyz:y = z ^ 2⊢ x = sin (z ^ 2)
  have : sin y = sin (z^2) := byx:ℝy:ℝz:ℝhxy:x = sin yhyz:y = z ^ 2⊢ x = sin (z ^ 2) rw [hyz]All goals completed! 🐙
  exact hxy.trans thisAll goals completed! 🐙

abbrev make_twelve_equal_two : ℤ → ℤ → Prop := fun a b ↦ a = 12 ∧ b = 2

A version of the integers where 12 has been forced to equal 2.

abbrev NewInt := Quot make_twelve_equal_two

A coercion from integers to new integers

instance : Coe ℤ NewInt where
  coe n := Quot.mk make_twelve_equal_two n

Quot.mk make_twelve_equal_two 2 : Quot make_twelve_equal_two#check ((2:ℤ):NewInt)

Quot.mk make_twelve_equal_two 2 : Quot make_twelve_equal_two

Quot.mk make_twelve_equal_two 12 : Quot make_twelve_equal_two#check ((12:ℤ):NewInt)

Quot.mk make_twelve_equal_two 12 : Quot make_twelve_equal_two

example : ((12:ℤ):NewInt) = ((2:ℤ):NewInt) := by⊢ Quot.mk make_twelve_equal_two 12 = Quot.mk make_twelve_equal_two 2
  apply Quot.sounda⊢ make_twelve_equal_two 12 2
  simp [make_twelve_equal_two]All goals completed! 🐙

theorem NewInt.is_coe (N:NewInt) : ∃ n:ℤ, N = (n:NewInt) := byN:NewInt⊢ ∃ n, N = Quot.mk make_twelve_equal_two n
  apply Quot.ind (q := N)N:NewInt⊢ ∀ (a : ℤ), ∃ n, Quot.mk make_twelve_equal_two a = Quot.mk make_twelve_equal_two n; intro nN:NewIntn:ℤ⊢ ∃ n_1, Quot.mk make_twelve_equal_two n = Quot.mk make_twelve_equal_two n_1
  use nAll goals completed! 🐙

abbrev NewInt.quot {X:Type} {f: ℤ → X} (hf: f 12 = f 2) : NewInt → X := byX:Typef:ℤ → Xhf:f 12 = f 2⊢ NewInt → X
  apply Quot.lift fX:Typef:ℤ → Xhf:f 12 = f 2⊢ ∀ (a b : ℤ), make_twelve_equal_two a b → f a = f b
  intro a bX:Typef:ℤ → Xhf:f 12 = f 2a:ℤb:ℤ⊢ make_twelve_equal_two a b → f a = f b
  simp [make_twelve_equal_two]X:Typef:ℤ → Xhf:f 12 = f 2a:ℤb:ℤ⊢ a = 12 → b = 2 → f a = f b
  intro ha hbX:Typef:ℤ → Xhf:f 12 = f 2a:ℤb:ℤha:a = 12hb:b = 2⊢ f a = f b
  rw [ha, hb, hf]All goals completed! 🐙

example {X:Type} {f:ℤ → X} (hf: f 12 = f 2) (n:ℤ) : NewInt.quot hf (n:NewInt) = f n := rfl

/-- Exercise A.7.1 -/
declaration uses `sorry`example {a b c d:ℝ} (hab: a = b) (hcd : c = d) : a + d = b + c := bya:ℝb:ℝc:ℝd:ℝhab:a = bhcd:c = d⊢ a + d = b + c
  sorryAll goals completed! 🐙