-- Mathlib/Order/KrullDimension.lean
lemma length_le_height {p : LTSeries α} {x : α} (hlast : p.last ≤ x) :
    p.length ≤ height x

Proof state:
case pos
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc x ⋯
⊢ ↑p'.length ≤ height x

Tactic:
refine le_iSup₂_of_le p' ?_ le_rfl

Result:
case pos
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc x ⋯
⊢ p'.last ≤ x

Proof state:
case hab
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ (RelSeries.eraseLast p).last < ?b

Tactic:
apply p.step ⟨p.length - 1, by omega⟩

Result:
no goals

Proof state:
case h.e'_3
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ p.toFun ⟨p.length - 1 + 1, ⋯⟩ = p.toFun ⟨p.length, ⋯⟩

Tactic:
congr

Result:
case h.e'_3.e_a.e_val
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ p.length - 1 + 1 = p.length

Proof state:
case h.e'_3.e_a.e_val
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ p.length - 1 + 1 = p.length

Tactic:
omega

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : ¬p.length ≠ 0
⊢ ↑p.length ≤ height x

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ (RelSeries.eraseLast p).last < x

Tactic:
apply lt_of_lt_of_le

Result:
case hab
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ (RelSeries.eraseLast p).last < ?b

case hbc
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ ?b ≤ x

case b
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ α

Proof state:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc x ⋯
this : ↑p'.length ≤ height x
⊢ ↑p.length ≤ height x

Tactic:
simp [p'] at this

Result:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc x ⋯
this : ↑p.length - 1 + 1 ≤ height x
⊢ ↑p.length ≤ height x

Proof state:
case pos
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc x ⋯
⊢ ↑p.length ≤ height x

Tactic:
suffices p'.length ≤ height x by
  simp [p'] at this
  convert this
  norm_cast
  omega

Result:
case pos
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc x ⋯
⊢ ↑p'.length ≤ height x

Proof state:
case pos
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc x ⋯
⊢ p'.last ≤ x

Tactic:
simp [p']

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
⊢ ↑p.length ≤ height x

Tactic:
by_cases hlen0 : p.length ≠ 0

Result:
case pos
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ ↑p.length ≤ height x

case neg
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : ¬p.length ≠ 0
⊢ ↑p.length ≤ height x

Proof state:
case h.e'_3
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc x ⋯
this : ↑p.length - 1 + 1 ≤ height x
⊢ p.length = p.length - 1 + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc x ⋯
this : ↑p.length - 1 + 1 ≤ height x
⊢ ↑p.length ≤ height x

Tactic:
convert this

Result:
case h.e'_3
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc x ⋯
this : ↑p.length - 1 + 1 ≤ height x
⊢ ↑p.length = ↑p.length - 1 + 1

Proof state:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ p.length - 1 < p.length

Tactic:
omega

Result:
no goals

Proof state:
case h.e'_3
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ p.toFun ⟨p.length - 1, ⋯⟩.succ = RelSeries.last p

Tactic:
simp only [Fin.succ_mk, Nat.succ_eq_add_one, RelSeries.last, Fin.last]

Result:
case h.e'_3
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ p.toFun ⟨p.length - 1 + 1, ⋯⟩ = p.toFun ⟨p.length, ⋯⟩

Proof state:
case hbc
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ p.toFun ⟨p.length - 1, ⋯⟩.succ ≤ x

Tactic:
convert hlast

Result:
case h.e'_3
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ p.toFun ⟨p.length - 1, ⋯⟩.succ = RelSeries.last p

Proof state:
case h.e'_3
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc x ⋯
this : ↑p.length - 1 + 1 ≤ height x
⊢ ↑p.length = ↑p.length - 1 + 1

Tactic:
norm_cast

Result:
case h.e'_3
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc x ⋯
this : ↑p.length - 1 + 1 ≤ height x
⊢ p.length = p.length - 1 + 1