-- Mathlib/Order/KrullDimension.lean
lemma coe_lt_height_iff {x : α} {n : ℕ} (hfin : height x < ⊤) :
    n < height x ↔ ∃ y < x, height y = n where
  mp h

Proof state:
case h.left
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ p.toFun ⟨n, ⋯⟩ < x

Tactic:
rw [← hp]

Result:
case h.left
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ p.toFun ⟨n, ⋯⟩ < RelSeries.last p

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ n < p.length + 1

Tactic:
omega

Result:
no goals

Proof state:
case h.left.a
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ ⟨n, ⋯⟩ < Fin.last p.length

Tactic:
simp [Fin.last]

Result:
case h.left.a
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ n < p.length

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ ∃ y < x, height y = ↑n

Tactic:
use p ⟨n, by omega⟩

Result:
case h
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ p.toFun ⟨n, ⋯⟩ < x ∧ height (p.toFun ⟨n, ⋯⟩) = ↑n

Proof state:
case h
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ p.toFun ⟨n, ⋯⟩ < x ∧ height (p.toFun ⟨n, ⋯⟩) = ↑n

Tactic:
constructor

Result:
case h.left
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ p.toFun ⟨n, ⋯⟩ < x

case h.right
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ height (p.toFun ⟨n, ⋯⟩) = ↑n

Proof state:
case h.left.a
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ n < p.length

Tactic:
omega

Result:
no goals

Proof state:
case h.right
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ height (p.toFun ⟨n, ⋯⟩) = ↑n

Tactic:
exact height_eq_index_of_length_eq_height_last (by simp [hlen, hp, hx]) ⟨n, by omega⟩

Result:
no goals

Proof state:
case h.left
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ p.toFun ⟨n, ⋯⟩ < RelSeries.last p

Tactic:
apply LTSeries.strictMono

Result:
case h.left.a
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ ⟨n, ⋯⟩ < Fin.last p.length

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
h : ↑n < height x
⊢ ∃ y < x, height y = ↑n

Tactic:
obtain ⟨m, hx : height x = m⟩ := Option.ne_none_iff_exists'.mp hfin.ne_top

Result:
case intro
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
h : ↑n < height x
m : ℕ
hx : height x = ↑m
⊢ ∃ y < x, height y = ↑n

Proof state:
case intro
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
h : ↑n < ↑m
hx : height x = ↑m
⊢ ∃ y < x, height y = ↑n

Tactic:
norm_cast at h

Result:
case intro
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
⊢ ∃ y < x, height y = ↑n

Proof state:
case intro
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
⊢ ∃ y < x, height y = ↑n

Tactic:
obtain ⟨p, hp, hlen⟩ := exists_series_of_height_eq_coe x hx

Result:
case intro.intro.intro
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ ∃ y < x, height y = ↑n

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ ↑p.length = height (RelSeries.last p)

Tactic:
simp [hlen, hp, hx]

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
h : ↑n < height x
m : ℕ
hx : height x = ↑m
⊢ ∃ y < x, height y = ↑n

Tactic:
rw [hx] at h

Result:
case intro
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
h : ↑n < ↑m
hx : height x = ↑m
⊢ ∃ y < x, height y = ↑n