ratRel

formal source

  44
  45/-- The field-of-fractions equivalence: `(a, b) ~ (c, d)` iff
  46`a * d = c * b`. -/
  47def ratRel : PreRat → PreRat → Prop :=
  48  fun p q => p.num * q.den = q.num * p.den
  49
  50theorem ratRel_refl : ∀ p : PreRat, ratRel p p := by
  51  intro p
  52  show p.num * p.den = p.num * p.den
  53  rfl
  54
  55theorem ratRel_symm : ∀ {p q : PreRat}, ratRel p q → ratRel q p := by
  56  intro p q h
  57  show q.num * p.den = p.num * q.den
  58  exact h.symm
  59
  60theorem ratRel_trans : ∀ {p q r : PreRat}, ratRel p q → ratRel q r → ratRel p r := by
  61  rintro ⟨a, b, hb⟩ ⟨c, d, hd⟩ ⟨e, f, hf⟩ hpq hqr
  62  -- hpq : a * d = c * b
  63  -- hqr : c * f = e * d
  64  -- goal: a * f = e * b
  65  -- Method: (a * f) * d = a * f * d = a * d * f = c * b * f = c * f * b = e * d * b = (e * b) * d.
  66  -- Cancel d ≠ 0.
  67  show a * f = e * b
  68  have key : (a * f) * d = (e * b) * d := by
  69    calc (a * f) * d
  70        = (a * d) * f := by rw [mul_assoc', mul_comm' f d, ← mul_assoc']
  71      _ = (c * b) * f := by rw [hpq]
  72      _ = (c * f) * b := by rw [mul_assoc', mul_comm' b f, ← mul_assoc']
  73      _ = (e * d) * b := by rw [hqr]
  74      _ = (e * b) * d := by rw [mul_assoc', mul_comm' d b, ← mul_assoc']
  75  exact mul_right_cancel hd key
  76
  77instance setoid : Setoid PreRat := ⟨ratRel, ratRel_refl, ratRel_symm, ratRel_trans⟩