English
A Zigzag in a discrete category implies equality of endpoints.
Русский
Zigzag в дискретной категории означает равенство концов.
LaTeX
$$$\forall X\ {a,b : \mathrm{Discrete}(X)},\ Zigzag\ a b \Rightarrow a.as = b.as$$$
Lean4
/-- A zigzag in a discrete category entails an equality of its extremities -/
theorem eq_of_zigzag (X) {a b : Discrete X} (h : Zigzag a b) : a.as = b.as := by
induction h with
| refl => rfl
| tail _ h eq =>
exact
eq.trans
(eq_of_zag _ h)
-- TODO: figure out the right way to generalise this to `Zigzag`.