pith. machine review for the scientific record. sign in
theorem proved tactic proof

ratRel_trans

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  60theorem ratRel_trans : ∀ {p q r : PreRat}, ratRel p q → ratRel q r → ratRel p r := by

proof body

Tactic-mode proof.

  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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.