-- Mathlib/Order/KrullDimension.lean
lemma krullDim_le_one_iff : krullDim α ≤ 1 ↔ ∀ x : α, IsMin x ∨ IsMax x

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : y < x
z : α
hzx : x < z
⊢ ∃ i, 1 < ↑i.length

Tactic:
exact ⟨⟨2, ![y, x, z], fun i ↦ by fin_cases i <;> simpa⟩, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : y < x
z : α
hzx : x < z
i : Fin 2
⊢ ![y, x, z] i.castSucc < ![y, x, z] i.succ

Tactic:
fin_cases i <;> simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : y < x
z : α
hzx : x < z
⊢ 1 < ↑{ length := 2, toFun := ![y, x, z], step := ⋯ }.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ (¬∀ (i : LTSeries α), ↑i.length ≤ 1) ↔ ¬∀ (x : α), (∀ (b : α), ¬b < x) ∨ ∀ (b : α), ¬x < b

Tactic:
push_neg

Result:
α : Type u_1
inst✝ : Preorder α
⊢ (∃ i, 1 < ↑i.length) ↔ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ ¬krullDim α ≤ 1 ↔ ¬∀ (x : α), IsMin x ∨ IsMax x

Tactic:
simp_rw [isMax_iff_forall_not_lt, isMin_iff_forall_not_lt, krullDim, iSup_le_iff]

Result:
α : Type u_1
inst✝ : Preorder α
⊢ (¬∀ (i : LTSeries α), ↑i.length ≤ 1) ↔ ¬∀ (x : α), (∀ (b : α), ¬b < x) ∨ ∀ (b : α), ¬x < b

Proof state:
case mp.intro.mk.succ.succ
α : Type u_1
inst✝ : Preorder α
n : ℕ
l : Fin (n + 1 + 1 + 1) → α
hl : ∀ (i : Fin (n + 1 + 1)), l i.castSucc < l i.succ
hl' : 1 < ↑{ length := n + 1 + 1, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

Tactic:
exact ⟨l 1, ⟨l 0, hl 0⟩, l 2, hl 1⟩

Result:
no goals

Proof state:
case mp.intro.mk.succ.zero
α : Type u_1
inst✝ : Preorder α
l : Fin (0 + 1 + 1) → α
hl : ∀ (i : Fin (0 + 1)), l i.castSucc < l i.succ
hl' : 1 < ↑{ length := 0 + 1, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

Tactic:
cases hl'.not_le (by simp)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
l : Fin (0 + 1 + 1) → α
hl : ∀ (i : Fin (0 + 1)), l i.castSucc < l i.succ
hl' : 1 < ↑{ length := 0 + 1, toFun := l, step := hl }.length
⊢ ↑{ length := 0 + 1, toFun := l, step := hl }.length ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ krullDim α ≤ 1 ↔ ∀ (x : α), IsMin x ∨ IsMax x

Tactic:
rw [← not_iff_not]

Result:
α : Type u_1
inst✝ : Preorder α
⊢ ¬krullDim α ≤ 1 ↔ ¬∀ (x : α), IsMin x ∨ IsMax x

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ (∃ i, 1 < ↑i.length) ↔ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : Preorder α
⊢ (∃ i, 1 < ↑i.length) → ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

case mpr
α : Type u_1
inst✝ : Preorder α
⊢ (∃ x, (∃ b, b < x) ∧ ∃ b, x < b) → ∃ i, 1 < ↑i.length

Proof state:
case mpr
α : Type u_1
inst✝ : Preorder α
⊢ (∃ x, (∃ b, b < x) ∧ ∃ b, x < b) → ∃ i, 1 < ↑i.length

Tactic:
rintro ⟨x, ⟨y, hxy⟩, z, hzx⟩

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : y < x
z : α
hzx : x < z
⊢ ∃ i, 1 < ↑i.length

Proof state:
case mp
α : Type u_1
inst✝ : Preorder α
⊢ (∃ i, 1 < ↑i.length) → ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

Tactic:
rintro ⟨⟨_ | _ | n, l, hl⟩, hl'⟩

Result:
case mp.intro.mk.zero
α : Type u_1
inst✝ : Preorder α
l : Fin (0 + 1) → α
hl : ∀ (i : Fin 0), l i.castSucc < l i.succ
hl' : 1 < ↑{ length := 0, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

case mp.intro.mk.succ.zero
α : Type u_1
inst✝ : Preorder α
l : Fin (0 + 1 + 1) → α
hl : ∀ (i : Fin (0 + 1)), l i.castSucc < l i.succ
hl' : 1 < ↑{ length := 0 + 1, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

case mp.intro.mk.succ.succ
α : Type u_1
inst✝ : Preorder α
n : ℕ
l : Fin (n + 1 + 1 + 1) → α
hl : ∀ (i : Fin (n + 1 + 1)), l i.castSucc < l i.succ
hl' : 1 < ↑{ length := n + 1 + 1, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b