Equality transitivity

2/4 ~15 minlean

Prove equality transitivity using rewriting or existing equality eliminators.

3 lines · Lean 4

theorem eq_trans_local {α : Type} (a b c : α)
    (hab : a = b) (hbc : b = c) : a = c := by
  sorry

Objectifs

Indices

Voir la solution

theorem eq_trans_local {α : Type} (a b c : α)
    (hab : a = b) (hbc : b = c) : a = c := by
  rw [hab]
  exact hbc