ext' — Mathlib

English

Two paths are equal if all their arrows are equal.

Русский

Два пути равны, если равны все их рёбра.

LaTeX

$$$\\forall f,g:\\, X.Path(m), (\\forall i, f.arrow i = g.arrow i) \\Rightarrow f = g$$$

Lean4

/-- To show two paths equal it suffices to show that they have the same edges. -/
@[ext]
theorem ext' {f g : Path X (m + 1)} (h : ∀ i, f.arrow i = g.arrow i) : f = g :=
  by
  ext j
  · rcases Fin.eq_castSucc_or_eq_last j with ⟨k, hk⟩ | hl
    · rw [hk, ← f.arrow_src k, ← g.arrow_src k, h]
    · simp only [hl, ← Fin.succ_last]
      rw [← f.arrow_tgt (Fin.last m), ← g.arrow_tgt (Fin.last m), h]
  · exact h j

Похожие утверждения