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

intRel_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)

  55theorem intRel_trans : ∀ {p q r : LogicNat × LogicNat},
  56    intRel p q → intRel q r → intRel p r := by

proof body

Tactic-mode proof.

  57  rintro ⟨a, b⟩ ⟨c, d⟩ ⟨e, f⟩ hpq hqr
  58  show a + f = e + b
  59  rw [eq_iff_toNat_eq, toNat_add, toNat_add]
  60  have hpq' : toNat a + toNat d = toNat c + toNat b := by
  61    have := congrArg toNat (show a + d = c + b from hpq)
  62    rwa [toNat_add, toNat_add] at this
  63  have hqr' : toNat c + toNat f = toNat e + toNat d := by
  64    have := congrArg toNat (show c + f = e + d from hqr)
  65    rwa [toNat_add, toNat_add] at this
  66  omega
  67
  68/-- The setoid structure on `LogicNat × LogicNat` for Grothendieck
  69completion. -/

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.