-- Mathlib/Order/KrullDimension.lean
@[simp] lemma coheight_of_noMaxOrder [NoMaxOrder α] (a : α) : coheight a = ⊤

Proof state:
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
⊢ (fun i => if i = 0 then a else ↑(f ↑i)) ⟨i, hi⟩.castSucc < (fun i => if i = 0 then a else ↑(f ↑i)) ⟨i, hi⟩.succ

Tactic:
suffices f i < f (i + 1) by simp [Fin.ext_iff, hzero, this]

Result:
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
⊢ f i < f (i + 1)

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m : ℕ
⊢ ∀ (i : Fin m), (fun i => if i = 0 then a else ↑(f ↑i)) i.castSucc < (fun i => if i = 0 then a else ↑(f ↑i)) i.succ

Tactic:
intro ⟨i, hi⟩

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
⊢ (fun i => if i = 0 then a else ↑(f ↑i)) ⟨i, hi⟩.castSucc < (fun i => if i = 0 then a else ↑(f ↑i)) ⟨i, hi⟩.succ

Proof state:
case neg.a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
⊢ i < i + 1

Tactic:
omega

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : i = 0
⊢ (fun i => if i = 0 then a else ↑(f ↑i)) ⟨i, hi⟩.castSucc < (fun i => if i = 0 then a else ↑(f ↑i)) ⟨i, hi⟩.succ

Tactic:
subst i

Result:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m : ℕ
hi : 0 < m
⊢ (fun i => if i = 0 then a else ↑(f ↑i)) ⟨0, hi⟩.castSucc < (fun i => if i = 0 then a else ↑(f ↑i)) ⟨0, hi⟩.succ

Proof state:
case intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
⊢ coheight a = ⊤

Tactic:
apply coheight_eq_top_iff.mpr

Result:
case intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
⊢ ∀ (n : ℕ), ∃ p, RelSeries.head p = a ∧ p.length = n

Proof state:
case h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m : ℕ
⊢ { length := m, toFun := fun i => if i = 0 then a else ↑(f ↑i), step := ?step }.head = a ∧
    { length := m, toFun := fun i => if i = 0 then a else ↑(f ↑i), step := ?step }.length = m

case step
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m : ℕ
⊢ ∀ (i : Fin m), (fun i => if i = 0 then a else ↑(f ↑i)) i.castSucc < (fun i => if i = 0 then a else ↑(f ↑i)) i.succ

Tactic:
case h => simp [RelSeries.head]

Result:
case step
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m : ℕ
⊢ ∀ (i : Fin m), (fun i => if i = 0 then a else ↑(f ↑i)) i.castSucc < (fun i => if i = 0 then a else ↑(f ↑i)) i.succ

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
⊢ (fun i => if i = 0 then a else ↑(f ↑i)) ⟨i, hi⟩.castSucc < (fun i => if i = 0 then a else ↑(f ↑i)) ⟨i, hi⟩.succ

Tactic:
by_cases hzero : i = 0

Result:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : i = 0
⊢ (fun i => if i = 0 then a else ↑(f ↑i)) ⟨i, hi⟩.castSucc < (fun i => if i = 0 then a else ↑(f ↑i)) ⟨i, hi⟩.succ

case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
⊢ (fun i => if i = 0 then a else ↑(f ↑i)) ⟨i, hi⟩.castSucc < (fun i => if i = 0 then a else ↑(f ↑i)) ⟨i, hi⟩.succ

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
⊢ coheight a = ⊤

Tactic:
obtain ⟨f, hstrictmono⟩ := Nat.exists_strictMono ↑(Set.Ioi a)

Result:
case intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
⊢ coheight a = ⊤

Proof state:
case intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
⊢ ∀ (n : ℕ), ∃ p, RelSeries.head p = a ∧ p.length = n

Tactic:
intro m

Result:
case intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m : ℕ
⊢ ∃ p, RelSeries.head p = a ∧ p.length = m

Proof state:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m : ℕ
hi : 0 < m
⊢ (fun i => if i = 0 then a else ↑(f ↑i)) ⟨0, hi⟩.castSucc < (fun i => if i = 0 then a else ↑(f ↑i)) ⟨0, hi⟩.succ

Tactic:
exact (f 1).prop

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
this : f i < f (i + 1)
⊢ (fun i => if i = 0 then a else ↑(f ↑i)) ⟨i, hi⟩.castSucc < (fun i => if i = 0 then a else ↑(f ↑i)) ⟨i, hi⟩.succ

Tactic:
simp [Fin.ext_iff, hzero, this]

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m : ℕ
⊢ ∃ p, RelSeries.head p = a ∧ p.length = m

Tactic:
use {length := m, toFun := fun i => if i = 0 then a else f i, step := ?step }

Result:
case h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m : ℕ
⊢ { length := m, toFun := fun i => if i = 0 then a else ↑(f ↑i), step := ?step }.head = a ∧
    { length := m, toFun := fun i => if i = 0 then a else ↑(f ↑i), step := ?step }.length = m

case step
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m : ℕ
⊢ ∀ (i : Fin m), (fun i => if i = 0 then a else ↑(f ↑i)) i.castSucc < (fun i => if i = 0 then a else ↑(f ↑i)) i.succ

Proof state:
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
⊢ f i < f (i + 1)

Tactic:
apply hstrictmono

Result:
case neg.a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
⊢ i < i + 1

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m : ℕ
⊢ { length := m, toFun := fun i => if i = 0 then a else ↑(f ↑i), step := ?step }.head = a ∧
    { length := m, toFun := fun i => if i = 0 then a else ↑(f ↑i), step := ?step }.length = m

Tactic:
simp [RelSeries.head]

Result:
no goals