English
Height a ≤ n iff all LTSeries ending at a have length ≤ n.
Русский
Высота a ≤ n тогда и только тогда, когда все LTSeries, оканчивающиеся в a, имеют длину ≤ n.
LaTeX
$$$\operatorname{height}(a) \le n \iff \forall p : LTSeries(\alpha), p.last = a \rightarrow p.length \le n.$$$
Lean4
theorem height_le {a : α} {n : ℕ∞} (h : ∀ (p : LTSeries α), p.last = a → p.length ≤ n) : height a ≤ n :=
by
apply height_le_iff.mpr
intro p hlast
wlog hlenpos : p.length ≠ 0
·
simp_all
-- We replace the last element in the series with `a`
let p' := p.eraseLast.snoc a (lt_of_lt_of_le (p.eraseLast_last_rel_last (by simp_all)) hlast)
rw [show p.length = p'.length by simp [p']; cutsat]
apply h
simp [p']
