-- 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' : LTSeries α :=
  { length := p.length - 1,
    toFun := fun x =>
      match x with
      | ⟨i, hi⟩ => (p.toFun ⟨i + 1, ⋯⟩).unbot ⋯,
    step := ⋯ }
⊢ ↑p.length ≤ height x + 1

Tactic:
have hlast' : p'.last = x := by
  simp only [p', RelSeries.last, Fin.val_last, WithBot.unbot_eq_iff, ← hlast, Fin.last]
  congr
  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 := ⋯ }
hlast' : RelSeries.last p' = x
⊢ ↑p.length ≤ height x + 1

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

Tactic:
wlog hlenpos : p.length ≠ 0

Result:
case a.h.inr
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
this :
  ∀ {α : Type u_1} [inst : Preorder α] (x : α) (p : LTSeries (WithBot α)),
    RelSeries.last p = ↑x → p.length ≠ 0 → ↑p.length ≤ height x + 1
hlenpos : ¬p.length ≠ 0
⊢ ↑p.length ≤ height x + 1

α✝ : 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

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hlast : RelSeries.last p = x
⊢ ⊥ < RelSeries.head (p.map (fun a => ↑a) ⋯)

Tactic:
simp

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
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, ⋯⟩

Tactic:
congr

Result:
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

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
⊢ RelSeries.head p < p.toFun ⟨i + 1, ⋯⟩

Tactic:
apply p.strictMono

Result:
case a
α✝ : 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
⊢ 0 < ⟨i + 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
x✝ : Fin (p.length - 1 + 1)
i : ℕ
hi : i < p.length - 1 + 1
⊢ i + 1 < p.length + 1

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
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
this : ↑p'.length ≤ height (RelSeries.last p')
⊢ ↑p.length ≤ height x + 1

Tactic:
simpa [p', hlast'] using this

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x + 1 ≤ height ↑x

Tactic:
rw [height_add_const]

Result:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p = x), ↑p.length + 1 ≤ height ↑x

Proof state:
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

Tactic:
apply le_iSup₂_of_le p' (by simp [p', hlast]) (by simp [p'])

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height ↑x = height x + 1

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height ↑x ≤ height x + 1

case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x + 1 ≤ height ↑x

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (p : LTSeries (WithBot α)), RelSeries.last p = ↑x → ↑p.length ≤ height x + 1

Tactic:
intro p hlast

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

Proof state:
case a
α✝ : 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
⊢ 0 < ⟨i + 1, ⋯⟩

Tactic:
exact compare_gt_iff_gt.mp rfl

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height ↑x ≤ height x + 1

Tactic:
apply height_le

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (p : LTSeries (WithBot α)), RelSeries.last p = ↑x → ↑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 := ⋯ }
hlast' : RelSeries.last p' = x
⊢ ↑p'.length ≤ height (RelSeries.last p')

Tactic:
apply length_le_height_last

Result:
no goals

Proof state:
α : 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 ≤ ↑p'.length

Tactic:
simp [p']

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
i : Fin (p.length - 1)
⊢ (fun x =>
        match x with
        | ⟨i, hi⟩ => (p.toFun ⟨i + 1, ⋯⟩).unbot ⋯)
      i.castSucc <
    (fun x =>
        match x with
        | ⟨i, hi⟩ => (p.toFun ⟨i + 1, ⋯⟩).unbot ⋯)
      i.succ

Tactic:
simpa [WithBot.unbot_lt_iff] using p.step ⟨i + 1, by omega⟩

Result:
no goals

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (i : LTSeries α), RelSeries.last i = x → ↑i.length + 1 ≤ height ↑x

Tactic:
intro p hlast

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

Proof state:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p = x), ↑p.length + 1 ≤ height ↑x

Tactic:
apply iSup₂_le

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (i : LTSeries α), RelSeries.last i = x → ↑i.length + 1 ≤ height ↑x

Proof state:
α : 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'.last ≤ ↑x

Tactic:
simp [p', hlast]

Result:
no goals

Proof state:
case a.h.inr
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
this :
  ∀ {α : Type u_1} [inst : Preorder α] (x : α) (p : LTSeries (WithBot α)),
    RelSeries.last p = ↑x → p.length ≠ 0 → ↑p.length ≤ height x + 1
hlenpos : ¬p.length ≠ 0
⊢ ↑p.length ≤ height x + 1

Tactic:
simp_all

Result:
no goals