-- Mathlib/Order/KrullDimension.lean
/-- The elements of finite height `n` are the minimal elements among those of height `≥ n`. -/
lemma height_eq_coe_iff_minimal_le_height {a : α} {n : ℕ} :
    height a = n ↔ Minimal (fun y => n ≤ height y) a

Proof state:
case pos.succ
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : height a < ⊤
n✝ : ℕ
hn : n = n✝ + 1
⊢ height a = ↑(n✝ + 1) ↔ Minimal (fun y => ↑(n✝ + 1) ≤ height y) a

Tactic:
simp [minimal_iff_forall_lt, height_eq_coe_add_one_iff, ENat.add_one_le_iff,
coe_lt_height_iff, *]

Result:
no goals

Proof state:
case pos.zero
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : height a < ⊤
hn : n = 0
⊢ height a = ↑0 ↔ Minimal (fun y => ↑0 ≤ height y) a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : ¬height a < ⊤
this : ∃ x < a, ↑n ≤ height x
⊢ height a = ↑n ↔ Minimal (fun y => ↑n ≤ height y) a

Tactic:
simp_all [minimal_iff_forall_lt]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : ¬height a < ⊤
⊢ height a = ↑n ↔ Minimal (fun y => ↑n ≤ height y) a

Tactic:
suffices ∃ x < a, ↑n ≤ height x by
  simp_all [minimal_iff_forall_lt]

Result:
case neg
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : ¬height a < ⊤
⊢ ∃ x < a, ↑n ≤ height x

Proof state:
α : Type u_1
inst✝ : Preorder α
n : ℕ
p : LTSeries α
hp : p.length = n + 1
hfin : ∀ (n : ℕ), ∃ p_1, RelSeries.last p_1 = RelSeries.last p ∧ p_1.length = n
⊢ p.length ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : ∀ (n : ℕ), ∃ p, RelSeries.last p = a ∧ p.length = n
⊢ ∃ x < a, ↑n ≤ height x

Tactic:
obtain ⟨p, rfl, hp⟩ := hfin (n+1)

Result:
case neg.intro.intro
α : Type u_1
inst✝ : Preorder α
n : ℕ
p : LTSeries α
hp : p.length = n + 1
hfin : ∀ (n : ℕ), ∃ p_1, RelSeries.last p_1 = RelSeries.last p ∧ p_1.length = n
⊢ ∃ x < RelSeries.last p, ↑n ≤ height x

Proof state:
case right
α : Type u_1
inst✝ : Preorder α
n : ℕ
p : LTSeries α
hp : p.length = n + 1
hfin : ∀ (n : ℕ), ∃ p_1, RelSeries.last p_1 = RelSeries.last p ∧ p_1.length = n
⊢ ↑n ≤ height (RelSeries.eraseLast p).last

Tactic:
simpa [hp] using length_le_height_last (p := p.eraseLast)

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : height a < ⊤
⊢ height a = ↑n ↔ Minimal (fun y => ↑n ≤ height y) a

Tactic:
cases hn : n with
| zero => simp
| succ => simp [minimal_iff_forall_lt, height_eq_coe_add_one_iff, ENat.add_one_le_iff,
    coe_lt_height_iff, *]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
⊢ height a = ↑n ↔ Minimal (fun y => ↑n ≤ height y) a

Tactic:
by_cases hfin : height a < ⊤

Result:
case pos
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : height a < ⊤
⊢ height a = ↑n ↔ Minimal (fun y => ↑n ≤ height y) a

case neg
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : ¬height a < ⊤
⊢ height a = ↑n ↔ Minimal (fun y => ↑n ≤ height y) a

Proof state:
case neg.intro.intro
α : Type u_1
inst✝ : Preorder α
n : ℕ
p : LTSeries α
hp : p.length = n + 1
hfin : ∀ (n : ℕ), ∃ p_1, RelSeries.last p_1 = RelSeries.last p ∧ p_1.length = n
⊢ ∃ x < RelSeries.last p, ↑n ≤ height x

Tactic:
use p.eraseLast.last, RelSeries.eraseLast_last_rel_last _ (by omega)

Result:
case right
α : Type u_1
inst✝ : Preorder α
n : ℕ
p : LTSeries α
hp : p.length = n + 1
hfin : ∀ (n : ℕ), ∃ p_1, RelSeries.last p_1 = RelSeries.last p ∧ p_1.length = n
⊢ ↑n ≤ height (RelSeries.eraseLast p).last

Proof state:
case neg
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : ¬height a < ⊤
⊢ ∃ x < a, ↑n ≤ height x

Tactic:
simp only [not_lt, top_le_iff, height_eq_top_iff] at hfin

Result:
case neg
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : ∀ (n : ℕ), ∃ p, RelSeries.last p = a ∧ p.length = n
⊢ ∃ x < a, ↑n ≤ height x