-- Mathlib/Order/KrullDimension.lean
lemma height_eq_krullDim_Iic (x : α) : (height x : ℕ∞) = krullDim (Set.Iic x)

Proof state:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
i✝ : RelSeries.last p ≤ ⊤
mono : StrictMono fun y => ↑y
⊢ ↑(p.map (fun x_1 => ↑x_1) mono).length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length

Tactic:
refine le_iSup₂ (f := fun p hp ↦ (p.length : ℕ∞)) (p.map (fun x ↦ x.1) mono) ?_

Result:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
i✝ : RelSeries.last p ≤ ⊤
mono : StrictMono fun y => ↑y
⊢ RelSeries.last (p.map (fun x_1 => ↑x_1) mono) ≤ x

Proof state:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p ≤ x
⊢ ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length

Tactic:
let q := LTSeries.mk p.length (fun i ↦ (⟨p.toFun i, le_trans (p.monotone (Fin.le_last _)) hp⟩
 : Set.Iic x)) (fun _ _ h ↦ p.strictMono h)

Result:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p ≤ x
q : LTSeries { x_1 // x_1 ∈ Set.Iic x } := LTSeries.mk p.length (fun i => ⟨p.toFun i, ⋯⟩) ⋯
⊢ ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (i : LTSeries α), ⨆ (_ : RelSeries.last i ≤ x), ↑i.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length

Tactic:
intro p

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
⊢ ⨆ (_ : RelSeries.last p ≤ x), ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length

Proof state:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
⊢ RelSeries.last p ≤ x → ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length

Tactic:
intro hp

Result:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p ≤ x
⊢ ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
⊢ ⨆ (_ : RelSeries.last p ≤ x), ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length

Tactic:
apply iSup_le

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

Proof state:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p ≤ x
q : LTSeries { x_1 // x_1 ∈ Set.Iic x } := LTSeries.mk p.length (fun i => ⟨p.toFun i, ⋯⟩) ⋯
⊢ ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length

Tactic:
simp only [le_top, iSup_pos, ge_iff_le]

Result:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p ≤ x
q : LTSeries { x_1 // x_1 ∈ Set.Iic x } := LTSeries.mk p.length (fun i => ⟨p.toFun i, ⋯⟩) ⋯
⊢ ↑p.length ≤ ⨆ p, ↑p.length

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ↑(height x) = krullDim ↑(Set.Iic x)

Tactic:
rw [← height_top_eq_krullDim, height, height, WithBot.coe_inj]

Result:
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length = ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length

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

Tactic:
apply le_antisymm

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

case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length

Proof state:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
i✝ : RelSeries.last p ≤ ⊤
⊢ ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length

Tactic:
have mono : StrictMono (fun (y : Set.Iic x) ↦ y.1) := fun _ _ h ↦ h

Result:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
i✝ : RelSeries.last p ≤ ⊤
mono : StrictMono fun y => ↑y
⊢ ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
⊢ ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length

Tactic:
apply iSup_le

Result:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
⊢ RelSeries.last p ≤ ⊤ → ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length

Proof state:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p ≤ x
q : LTSeries { x_1 // x_1 ∈ Set.Iic x } := LTSeries.mk p.length (fun i => ⟨p.toFun i, ⋯⟩) ⋯
⊢ ↑p.length ≤ ⨆ p, ↑p.length

Tactic:
exact le_iSup (fun p ↦ (p.length : ℕ∞)) q

Result:
no goals

Proof state:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
i✝ : RelSeries.last p ≤ ⊤
mono : StrictMono fun y => ↑y
⊢ ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length

Tactic:
rw [← LTSeries.map_length p (fun x ↦ x.1) mono, ]

Result:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
i✝ : RelSeries.last p ≤ ⊤
mono : StrictMono fun y => ↑y
⊢ ↑(p.map (fun x_1 => ↑x_1) mono).length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length

Proof state:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
i✝ : RelSeries.last p ≤ ⊤
mono : StrictMono fun y => ↑y
⊢ RelSeries.last (p.map (fun x_1 => ↑x_1) mono) ≤ x

Tactic:
exact (p.toFun (Fin.last p.length)).2

Result:
no goals

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

Tactic:
apply iSup_le

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (i : LTSeries α), ⨆ (_ : RelSeries.last i ≤ x), ↑i.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (i : LTSeries ↑(Set.Iic x)), ⨆ (_ : RelSeries.last i ≤ ⊤), ↑i.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length

Tactic:
intro p

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
⊢ ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length

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

Tactic:
apply iSup_le

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (i : LTSeries ↑(Set.Iic x)), ⨆ (_ : RelSeries.last i ≤ ⊤), ↑i.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length

Proof state:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
⊢ RelSeries.last p ≤ ⊤ → ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length

Tactic:
intro _

Result:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
i✝ : RelSeries.last p ≤ ⊤
⊢ ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length