-- Mathlib/Order/KrullDimension.lean
@[simp] lemma height_coe_withBot (x : α) : height (x : WithBot α) = height x + 1

Proof state:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
⊢ ↑p.length ≤ height x + 1

Tactic:
let p' : LTSeries α := {
  length := p.length - 1
  toFun := fun ⟨i, hi⟩ => (p ⟨i+1, by omega⟩).unbot (by
    apply LT.lt.ne_bot (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 omega⟩ }

Result:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
p' : LTSeries α :=
  { length := p.length - 1,
    toFun := fun x =>
      match x with
      | ⟨i, hi⟩ => (p.toFun ⟨i + 1, ⋯⟩).unbot ⋯,
    step := ⋯ }
⊢ ↑p.length ≤ height x + 1

Proof state:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
p' : LTSeries α :=
  { length := p.length - 1,
    toFun := fun x =>
      match x with
      | ⟨i, hi⟩ => (p.toFun ⟨i + 1, ⋯⟩).unbot ⋯,
    step := ⋯ }
⊢ RelSeries.last p' = x

Tactic:
simp only [p', RelSeries.last, Fin.val_last, WithBot.unbot_eq_iff, ← hlast, Fin.last]

Result:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
p' : LTSeries α :=
  { length := p.length - 1,
    toFun := fun x =>
      match x with
      | ⟨i, hi⟩ => (p.toFun ⟨i + 1, ⋯⟩).unbot ⋯,
    step := ⋯ }
⊢ p.toFun ⟨p.length - 1 + 1, ⋯⟩ = p.toFun ⟨p.length, ⋯⟩

Proof state:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
i : Fin (p.length - 1)
⊢ ↑i + 1 < p.length

Tactic:
omega

Result:
no goals

Proof state:
case e_a.e_val
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
p' : LTSeries α :=
  { length := p.length - 1,
    toFun := fun x =>
      match x with
      | ⟨i, hi⟩ => (p.toFun ⟨i + 1, ⋯⟩).unbot ⋯,
    step := ⋯ }
⊢ p.length - 1 + 1 = p.length

Tactic:
omega

Result:
no goals

Proof state:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
x✝ : Fin (p.length - 1 + 1)
i : ℕ
hi : i < p.length - 1 + 1
⊢ p.toFun ⟨i + 1, ⋯⟩ ≠ ⊥

Tactic:
apply LT.lt.ne_bot (a := p.head)

Result:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
x✝ : Fin (p.length - 1 + 1)
i : ℕ
hi : i < p.length - 1 + 1
⊢ RelSeries.head p < p.toFun ⟨i + 1, ⋯⟩

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hlast : RelSeries.last p = x
⊢ ↑p.length + 1 ≤ height ↑x

Tactic:
let p' := (p.map _ WithBot.coe_strictMono).cons ⊥ (by simp)

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hlast : RelSeries.last p = x
p' : RelSeries fun x1 x2 => x1 < x2 := RelSeries.cons (p.map (fun a => ↑a) ⋯) ⊥ ⋯
⊢ ↑p.length + 1 ≤ height ↑x

Proof state:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
p' : LTSeries α :=
  { length := p.length - 1,
    toFun := fun x =>
      match x with
      | ⟨i, hi⟩ => (p.toFun ⟨i + 1, ⋯⟩).unbot ⋯,
    step := ⋯ }
hlast' : RelSeries.last p' = x
⊢ ↑p.length ≤ height x + 1

Tactic:
suffices p'.length ≤ height p'.last by
  simpa [p', hlast'] using this

Result:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
p' : LTSeries α :=
  { length := p.length - 1,
    toFun := fun x =>
      match x with
      | ⟨i, hi⟩ => (p.toFun ⟨i + 1, ⋯⟩).unbot ⋯,
    step := ⋯ }
hlast' : RelSeries.last p' = x
⊢ ↑p'.length ≤ height (RelSeries.last p')