English
If p and q have the same length and agree on all getVert up to p.length, then p = q.
Русский
Если длины ходов p и q равны и они совпадают в своих вершинах на всех позициях до p.length, то p = q.
LaTeX
$$$ p.length = q.length \\rightarrow (\\forall k \\le p.length, p.getVert k = q.getVert k) \\rightarrow p = q $$$
Lean4
theorem ext_getVert_le_length {u v} {p q : G.Walk u v} (hl : p.length = q.length)
(h : ∀ k ≤ p.length, p.getVert k = q.getVert k) : p = q :=
by
suffices ∀ k : ℕ, p.support[k]? = q.support[k]? by exact ext_support <| List.ext_getElem?_iff.mpr this
intro k
cases le_or_gt k p.length with
| inl hk =>
rw [← getVert_eq_support_getElem? p hk, ← getVert_eq_support_getElem? q (hl ▸ hk)]
exact congrArg some (h k hk)
| inr hk =>
replace hk : p.length + 1 ≤ k := hk
have ht : q.length + 1 ≤ k := hl ▸ hk
rw [← length_support, ← List.getElem?_eq_none_iff] at hk ht
rw [hk, ht]
