English
Same as Height Index Theorem: height(p(i)) = i for p.length = height(p.last).
Русский
То же самое, что и Высота‑индекс: height(p(i)) = i при p.length = height(p.last).
LaTeX
$$$p.length = \operatorname{height}(p.last) \Rightarrow \forall i : Fin(p.length + 1), \operatorname{height}(p(i)) = i.$$$
Lean4
/-- In a maximally long series, i.e one as long as the height of the last element, the height of each
element is its index in the series.
-/
theorem height_eq_index_of_length_eq_height_last {p : LTSeries α} (h : p.length = height p.last)
(i : Fin (p.length + 1)) : height (p i) = i :=
by
refine le_antisymm (height_le ?_) (index_le_height p i)
intro p' hp'
have hp'' := length_le_height_last (p := p'.smash (p.drop i) (by simpa))
simp [← h] at hp''; clear h
norm_cast at *
cutsat