English
For any a ∈ α and n ∈ ℕ with n ≤ height a, there exists a LTSeries p with head a and length n.
Русский
Для любого a ∈ α и n ∈ ℕ при n ≤ height(a) существует LTSeries p с head = a и length = n.
LaTeX
$$$ \exists p:\ LTSeries\alpha,\ p.head = a ∧ p.length = n $$$
Lean4
/-- There exist a series ending in a element for any length up to the element’s height. -/
theorem exists_series_of_le_height (a : α) {n : ℕ} (h : n ≤ height a) : ∃ p : LTSeries α, p.last = a ∧ p.length = n :=
by
have hne : Nonempty { p : LTSeries α // p.last = a } := ⟨RelSeries.singleton _ a, rfl⟩
cases ha : height a with
| top =>
clear h
rw [height_eq_iSup_last_eq, iSup_subtype', ENat.iSup_coe_eq_top, bddAbove_def] at ha
contrapose! ha
use n
rintro m ⟨⟨p, rfl⟩, hp⟩
simp only at hp
by_contra! hnm
apply ha (p.drop ⟨m - n, by cutsat⟩) (by simp) (by simp; cutsat)
| coe m =>
rw [ha, Nat.cast_le] at h
rw [height_eq_iSup_last_eq, iSup_subtype'] at ha
obtain ⟨⟨p, hlast⟩, hlen⟩ := exists_eq_iSup_of_iSup_eq_coe ha
simp only [Nat.cast_inj] at hlen
use p.drop ⟨m - n, by cutsat⟩
constructor
· simp [hlast]
· simp [hlen]; cutsat
