English
For any x in α, height of x considered as an element of WithBot α equals height(x) + 1; i.e., embedding into WithBot increases height by one.
Русский
Для любого x в α высота x как элемента WithBot α равна height(x) + 1; то есть вставка в WithBot увеличивает высоту на единицу.
LaTeX
$$$$\\operatorname{height}(x : \\mathrm{WithBot}\\, \\alpha) = \\operatorname{height}(x) + 1.$$$$
Lean4
@[simp]
theorem height_coe_withBot (x : α) : height (x : WithBot α) = height x + 1 :=
by
apply le_antisymm
· apply height_le
intro p hlast
wlog hlenpos : p.length ≠ 0
·
simp_all
-- essentially p' := (p.drop 1).map unbot
let p' : LTSeries α :=
{ length := p.length - 1
toFun := fun ⟨i, hi⟩ =>
(p ⟨i + 1, by cutsat⟩).unbot
(by
apply ne_bot_of_gt (a := p.head)
apply p.strictMono
exact compare_gt_iff_gt.mp rfl)
step := fun i => by simpa [WithBot.unbot_lt_iff] using p.step ⟨i + 1, by cutsat⟩ }
have hlast' : p'.last = x :=
by
simp only [p', RelSeries.last, WithBot.unbot_eq_iff, ← hlast, Fin.last]
congr
omega
suffices p'.length ≤ height p'.last by simpa [p', hlast'] using this
apply length_le_height_last
· rw [height_add_const]
apply iSup₂_le
intro p hlast
let p' := (p.map _ WithBot.coe_strictMono).cons ⊥ (by simp)
apply le_iSup₂_of_le p' (by simp [p', hlast]) (by simp [p'])
