-- Mathlib/Order/KrullDimension.lean
@[simp] lemma height_coe_withTop (x : α) : height (x : WithTop α) = height x

Proof state:
case hab
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ p.toFun i ≤ ?b

Tactic:
exact p.monotone (Fin.le_last _)

Result:
no goals

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

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
p' : LTSeries α := { length := p.length, toFun := fun i => (p.toFun i).untop ⋯, step := ⋯ }
hlast' : RelSeries.last p' = x
⊢ ↑p.length ≤ height x

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

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
p' : LTSeries α := { length := p.length, toFun := fun i => (p.toFun i).untop ⋯, step := ⋯ }
hlast' : RelSeries.last p' = x
⊢ ↑p'.length ≤ height (RelSeries.last p')

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ p.toFun i < ⊤

Tactic:
apply lt_of_le_of_lt

Result:
case hab
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ p.toFun i ≤ ?b

case hbc
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ ?b < ⊤

case b
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ WithTop α

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

Tactic:
apply height_le

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

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
p' : LTSeries α := { length := p.length, toFun := fun i => (p.toFun i).untop ⋯, step := ⋯ }
hlast' : RelSeries.last p' = x
this : ↑p'.length ≤ height x
⊢ ↑p.length ≤ height x

Tactic:
simpa [p'] using this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hlast : RelSeries.last p = x
p' : LTSeries (WithTop α) := p.map (fun a => ↑a) ⋯
⊢ ↑p.length ≤ ↑p'.length

Tactic:
simp [p']

Result:
no goals

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

Tactic:
apply height_le

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

Proof state:
case hbc
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ p.toFun (Fin.last p.length) < ⊤

Tactic:
rw [RelSeries.last] at hlast

Result:
case hbc
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : p.toFun (Fin.last p.length) = ↑x
i : Fin (p.length + 1)
⊢ p.toFun (Fin.last p.length) < ⊤

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

Tactic:
apply le_antisymm

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

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

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
p' : LTSeries α := { length := p.length, toFun := fun i => (p.toFun i).untop ⋯, step := ⋯ }
⊢ RelSeries.last p' = x

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

Result:
no goals

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

Tactic:
let p' := p.map _ WithTop.coe_strictMono

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hlast : RelSeries.last p = x
p' : LTSeries (WithTop α) := p.map (fun a => ↑a) ⋯
⊢ ↑p.length ≤ height ↑x

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
p' : LTSeries α := { length := p.length, toFun := fun i => (p.toFun i).untop ⋯, 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 (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin p.length
⊢ (fun i => (p.toFun i).untop ⋯) i.castSucc < (fun i => (p.toFun i).untop ⋯) i.succ

Tactic:
simpa only [WithTop.untop_lt_iff, WithTop.coe_untop] using p.step i

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ p.toFun i ≠ ⊤

Tactic:
apply WithTop.lt_top_iff_ne_top.mp

Result:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin (p.length + 1)
⊢ p.toFun i < ⊤

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

Tactic:
simp [p', hlast]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
p' : LTSeries α := { length := p.length, toFun := fun i => (p.toFun i).untop ⋯, step := ⋯ }
hlast' : RelSeries.last p' = x
this : ↑p'.length ≤ height (RelSeries.last p')
⊢ ↑p.length ≤ height x

Tactic:
rw [hlast'] at this

Result:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
p' : LTSeries α := { length := p.length, toFun := fun i => (p.toFun i).untop ⋯, step := ⋯ }
hlast' : RelSeries.last p' = x
this : ↑p'.length ≤ height x
⊢ ↑p.length ≤ height x

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
p' : LTSeries α := { length := p.length, toFun := fun i => (p.toFun i).untop ⋯, step := ⋯ }
⊢ ↑p.length ≤ height x

Tactic:
have hlast' : p'.last = x := by
  simp only [p', RelSeries.last, Fin.val_last, WithTop.untop_eq_iff, ← hlast]

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
p' : LTSeries α := { length := p.length, toFun := fun i => (p.toFun i).untop ⋯, step := ⋯ }
hlast' : RelSeries.last p' = x
⊢ ↑p.length ≤ height x

Proof state:
case hbc
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : p.toFun (Fin.last p.length) = ↑x
i : Fin (p.length + 1)
⊢ p.toFun (Fin.last p.length) < ⊤

Tactic:
simp [hlast]

Result:
no goals

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

Tactic:
intro p hlast

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

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hlast : RelSeries.last p = x
p' : LTSeries (WithTop α) := p.map (fun a => ↑a) ⋯
⊢ ↑p.length ≤ height ↑x

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

Result:
no goals