English
Let x ∈ α and n ∈ ℕ. Then height x = n iff height x < ⊤ and (n = 0 or ∃ y < x with height y = n − 1) and (∀ y < x, height y < n).
Русский
Пусть x ∈ α и n ∈ ℕ. Тогда height(x) = n тогда и только если height(x) < ⊤ и (n = 0 или ∃ y < x с height(y) = n − 1) и (∀ y < x, height(y) < n).
LaTeX
$$$$ \operatorname{height}(x) = n \iff \big( \operatorname{height}(x) < \top \land \big( (n = 0) \lor (\exists y < x, \operatorname{height}(y) = n - 1) \big) \land \big( \forall y < x, \operatorname{height}(y) < n \big) \big) $$$$
Lean4
theorem height_eq_coe_iff {x : α} {n : ℕ} :
height x = n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = n - 1) ∧ (∀ y < x, height y < n) :=
by
wlog hfin : height x < ⊤
· simp_all
simp only [hfin, true_and]
cases n
case zero => simp [isMin_iff_forall_not_lt]
case succ n =>
simp only [Nat.cast_add, Nat.cast_one, add_eq_zero, one_ne_zero, and_false, false_or]
rw [height_eq_coe_add_one_iff]
simp only [hfin, true_and]
congr! 3
rename_i y _
cases height y <;> simp; norm_cast; cutsat
