-- Mathlib/Order/KrullDimension.lean
@[simp] lemma krullDim_of_isSimpleOrder {α : Type*} [PartialOrder α] [BoundedOrder α]
    [IsSimpleOrder α] : krullDim α = 1

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
p : LTSeries α
h : 1 < p.length
h2 : 2 < p.length + 1
h0' : 0 < p.length
h1 : 1 < p.length + 1
this✝ : p.toFun ⟨1, h1⟩ = ⊤
this : p.toFun ⟨1, h1⟩ < p.toFun ⟨2, h2⟩
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
p : LTSeries α
h : 1 < p.length
⊢ False

Tactic:
have h2 : 2 < p.length + 1 := add_lt_add_of_lt_of_le h (le_refl 1)

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
p : LTSeries α
h : 1 < p.length
h2 : 2 < p.length + 1
⊢ False

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
⊢ ⨆ p, ↑p.length = 1

Tactic:
refine le_antisymm (iSup_le fun p ↦ ?_) (le_iSup (fun p ↦ (p.length : WithBot ℕ∞)) q)

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
p : LTSeries α
⊢ ↑p.length ≤ 1

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ krullDim α = 1

Tactic:
rw [krullDim]

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⨆ p, ↑p.length = 1

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ∀ (i : Fin 1),
    (fun n => if (n == 0) = true then ⊥ else ⊤) i.castSucc < (fun n => if (n == 0) = true then ⊥ else ⊤) i.succ

Tactic:
simp [Fin.fin_one_eq_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
p : LTSeries α
h : 1 < p.length
h2 : 2 < p.length + 1
⊢ 0 < 1

Tactic:
decide

Result:
no goals

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
p : LTSeries α
h : 1 < p.length
h2 : 2 < p.length + 1
h0' : 0 < p.length
h1 : 1 < p.length + 1
⊢ False

Tactic:
have : p ⟨1, h1⟩ = ⊤ := IsSimpleOrder.eq_top_of_lt (p.step ⟨0, h0'⟩)

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
p : LTSeries α
h : 1 < p.length
h2 : 2 < p.length + 1
h0' : 0 < p.length
h1 : 1 < p.length + 1
this : p.toFun ⟨1, h1⟩ = ⊤
⊢ False

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
p : LTSeries α
⊢ ↑p.length ≤ 1

Tactic:
by_contra h

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
p : LTSeries α
h : ¬↑p.length ≤ 1
⊢ False

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
p : LTSeries α
h : 1 < p.length
h2 : 2 < p.length + 1
h0' : 0 < p.length
h1 : 1 < p.length + 1
this : p.toFun ⟨1, h1⟩ = ⊤
⊢ False

Tactic:
have : p ⟨1, h1⟩ < p ⟨2, h2⟩ := p.step ⟨1, h⟩

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
p : LTSeries α
h : 1 < p.length
h2 : 2 < p.length + 1
h0' : 0 < p.length
h1 : 1 < p.length + 1
this✝ : p.toFun ⟨1, h1⟩ = ⊤
this : p.toFun ⟨1, h1⟩ < p.toFun ⟨2, h2⟩
⊢ False

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⨆ p, ↑p.length = 1

Tactic:
let q : LTSeries α := ⟨1, (fun n ↦ if n == 0 then ⊥ else ⊤), by simp [Fin.fin_one_eq_zero]⟩

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
⊢ ⨆ p, ↑p.length = 1

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
p : LTSeries α
h : 1 < p.length
h2 : 2 < p.length + 1
h0' : 0 < p.length
⊢ 1 ≤ 2

Tactic:
decide

Result:
no goals

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
p : LTSeries α
h : ¬↑p.length ≤ 1
⊢ False

Tactic:
simp only [Nat.cast_le_one, not_le] at h

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
p : LTSeries α
h : 1 < p.length
⊢ False

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
p : LTSeries α
h : 1 < p.length
h2 : 2 < p.length + 1
⊢ False

Tactic:
have h0' : 0 < p.length := lt_trans (show 0 < 1 by decide) h

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
p : LTSeries α
h : 1 < p.length
h2 : 2 < p.length + 1
h0' : 0 < p.length
⊢ False

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
p : LTSeries α
h : 1 < p.length
h2 : 2 < p.length + 1
h0' : 0 < p.length
⊢ False

Tactic:
have h1 : 1 < p.length + 1 := lt_of_le_of_lt (show 1 ≤ 2 by decide) h2

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
q : LTSeries α := { length := 1, toFun := fun n => if (n == 0) = true then ⊥ else ⊤, step := ⋯ }
p : LTSeries α
h : 1 < p.length
h2 : 2 < p.length + 1
h0' : 0 < p.length
h1 : 1 < p.length + 1
⊢ False