mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h.left
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : p.length = m
⊢ (RelSeries.drop p ⟨m - n, ⋯⟩).last = a

pp: case h.right
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : p.length = m
⊢ (RelSeries.drop p ⟨m - n, ⋯⟩).length = n

Tactic:
·

Goal state after:
case h.left
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : p.length = m
⊢ (RelSeries.drop p ⟨m - n, ⋯⟩).last = a
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h.right
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : p.length = m
⊢ (RelSeries.drop p ⟨m - n, ⋯⟩).length = n

Tactic:
·

Goal state after:
case h.right
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : p.length = m
⊢ (RelSeries.drop p ⟨m - n, ⋯⟩).length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x ≤ ⨆ y, ⨆ (_ : y < x), height y + 1

pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ y, ⨆ (_ : y < x), height y + 1 ≤ height x

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x ≤ ⨆ y, ⨆ (_ : y < x), height y + 1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ p.length ≠ 0

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ y, ⨆ (_ : y < x), height y + 1 ≤ height x

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ y, ⨆ (_ : y < x), height y + 1 ≤ height x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
y : α
a✝ : y < x
⊢ ⊤ + 1 ≤ ↑n ↔ ⊤ < ↑n

pp: case coe
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
y : α
a✝¹ : y < x
a✝ : ℕ
⊢ ↑a✝ + 1 ≤ ↑n ↔ ↑a✝ < ↑n

Tactic:
·

Goal state after:
case top
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
y : α
a✝ : y < x
⊢ ⊤ + 1 ≤ ↑n ↔ ⊤ < ↑n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
y : α
a✝¹ : y < x
a✝ : ℕ
⊢ ↑a✝ + 1 ≤ ↑n ↔ ↑a✝ < ↑n

Tactic:
·

Goal state after:
case coe
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
y : α
a✝¹ : y < x
a✝ : ℕ
⊢ ↑a✝ + 1 ≤ ↑n ↔ ↑a✝ < ↑n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
⊢ 0 < height x ↔ ¬IsMin x

Tactic:
simp [pos_iff_ne_zero]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
⊢ 0 < coheight x ↔ ¬IsMax x

Tactic:
simp [pos_iff_ne_zero]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ n < p.length + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h.left
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ p.toFun ⟨n, ⋯⟩ < x

pp: case h.right
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ height (p.toFun ⟨n, ⋯⟩) = ↑n

Tactic:
·

Goal state after:
case h.left
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ p.toFun ⟨n, ⋯⟩ < x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h.right
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ height (p.toFun ⟨n, ⋯⟩) = ↑n

Tactic:
·

Goal state after:
case h.right
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ height (p.toFun ⟨n, ⋯⟩) = ↑n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ},
    height x < ⊤ → (height x = ↑n + 1 ↔ height x < ⊤ ∧ (∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n)
hfin : ¬height x < ⊤
⊢ height x = ↑n + 1 ↔ height x < ⊤ ∧ (∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n

pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x = ↑n + 1 ↔ height x < ⊤ ∧ (∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ},
    height x < ⊤ → (height x = ↑n + 1 ↔ height x < ⊤ ∧ (∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n)
hfin : ¬height x < ⊤
⊢ height x = ↑n + 1 ↔ height x < ⊤ ∧ (∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x = ↑n + 1 ↔ ↑n < height x ∧ height x ≤ ↑n + 1

pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ ↑n < height x ∧ height x ≤ ↑n + 1 ↔ (∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n

Tactic:
·

Goal state after:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x = ↑n + 1 ↔ ↑n < height x ∧ height x ≤ ↑n + 1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ ↑n < height x ∧ height x ≤ ↑n + 1 ↔ (∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n

Tactic:
·

Goal state after:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ ↑n < height x ∧ height x ≤ ↑n + 1 ↔ (∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case e'_1
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ ↑n < height x ↔ ∃ y < x, height y = ↑n

pp: case e'_2
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x ≤ ↑n + 1 ↔ ∀ y < x, height y ≤ ↑n

Tactic:
·

Goal state after:
case e'_1
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ ↑n < height x ↔ ∃ y < x, height y = ↑n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case e'_2
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x ≤ ↑n + 1 ↔ ∀ y < x, height y ≤ ↑n

Tactic:
·

Goal state after:
case e'_2
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x ≤ ↑n + 1 ↔ ∀ y < x, height y ≤ ↑n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ},
    height x < ⊤ → (height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n)
hfin : ¬height x < ⊤
⊢ height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n

pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ},
    height x < ⊤ → (height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n)
hfin : ¬height x < ⊤
⊢ height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : height a < ⊤
⊢ height a = ↑n ↔ Minimal (fun y ↦ ↑n ≤ height y) a

pp: case neg
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : ⊤ ≤ height a
⊢ height a = ↑n ↔ Minimal (fun y ↦ ↑n ≤ height y) a

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : height a < ⊤
⊢ height a = ↑n ↔ Minimal (fun y ↦ ↑n ≤ height y) a
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case neg
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : ⊤ ≤ height a
⊢ height a = ↑n ↔ Minimal (fun y ↦ ↑n ≤ height y) a

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : ⊤ ≤ height a
⊢ height a = ↑n ↔ Minimal (fun y ↦ ↑n ≤ height y) a
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
p : LTSeries α
hp : p.length = n + 1
hfin : ∀ (n : ℕ), ∃ p_1, RelSeries.last p_1 = RelSeries.last p ∧ p_1.length = n
⊢ p.length ≠ 0

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
x : α
h : 2 ≤ height x
⊢ ∃ y, ∃ z < y, y < x

pp: case refine_2
α : Type u_1
inst✝ : Preorder α
x : α
⊢ (∃ y, ∃ z < y, y < x) → 2 ≤ height x

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝ : Preorder α
x : α
h : 2 ≤ height x
⊢ ∃ y, ∃ z < y, y < x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
x : α
⊢ (∃ y, ∃ z < y, y < x) → 2 ≤ height x

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
x : α
⊢ (∃ y, ∃ z < y, y < x) → 2 ≤ height x
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inr
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
this :
  ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [WellFoundedLT α] [WellFoundedGT α]
    (s : LTSeries α), RelSeries.head s = ⊥ → ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
h₁ : ¬RelSeries.head s = ⊥
⊢ ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤

pp: α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
⊢ ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤

Tactic:
·

Goal state after:
case inr
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
this :
  ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [WellFoundedLT α] [WellFoundedGT α]
    (s : LTSeries α), RelSeries.head s = ⊥ → ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
h₁ : ¬RelSeries.head s = ⊥
⊢ ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ (∀ (x b : α), ¬x < b) → ∀ (i : LTSeries α), ↑i.length ≤ 0

Tactic:
·

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ (∀ (x b : α), ¬x < b) → ∀ (i : LTSeries α), ↑i.length ≤ 0
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Preorder α
H : ∀ (x b : α), ¬x < b
l : Fin (0 + 1) → α
h : ∀ (i : Fin 0), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
⊢ ↑{ length := 0, toFun := l, step := h }.length ≤ 0

pp: case succ
α : Type u_1
inst✝ : Preorder α
H : ∀ (x b : α), ¬x < b
n : ℕ
l : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
⊢ ↑{ length := n + 1, toFun := l, step := h }.length ≤ 0

Tactic:
·

Goal state after:
case zero
α : Type u_1
inst✝ : Preorder α
H : ∀ (x b : α), ¬x < b
l : Fin (0 + 1) → α
h : ∀ (i : Fin 0), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
⊢ ↑{ length := 0, toFun := l, step := h }.length ≤ 0
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Preorder α
H : ∀ (x b : α), ¬x < b
n : ℕ
l : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
⊢ ↑{ length := n + 1, toFun := l, step := h }.length ≤ 0

Tactic:
·

Goal state after:
case succ
α : Type u_1
inst✝ : Preorder α
H : ∀ (x b : α), ¬x < b
n : ℕ
l : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
⊢ ↑{ length := n + 1, toFun := l, step := h }.length ≤ 0
Module: Mathlib.Order.KrullDimension

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

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

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝ : Preorder α
⊢ (∃ i, 1 < ↑i.length) → ∃ x, (∃ b, b < x) ∧ ∃ b, x < b
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inr
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
this :
  ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [WellFoundedLT α] [WellFoundedGT α]
    (s : LTSeries α),
    RelSeries.head s = ⊥ → RelSeries.last s = ⊤ → ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
h₂ : ¬RelSeries.last s = ⊤
⊢ ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤

pp: α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
⊢ ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤

Tactic:
·

Goal state after:
case inr
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
this :
  ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [WellFoundedLT α] [WellFoundedGT α]
    (s : LTSeries α),
    RelSeries.head s = ⊥ → RelSeries.last s = ⊤ → ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
h₂ : ¬RelSeries.last s = ⊤
⊢ ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
Module: Mathlib.Order.KrullDimension

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

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

pp: case mp.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) ∈ {(a, b) | a < b}
hl' : 1 < ↑{ length := n + 1 + 1, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

Tactic:
·

Goal state after:
case mp.zero
α : Type u_1
inst✝ : Preorder α
l : Fin (0 + 1) → α
hl : ∀ (i : Fin 0), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
hl' : 1 < ↑{ length := 0, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b
Module: Mathlib.Order.KrullDimension

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

pp: case mp.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) ∈ {(a, b) | a < b}
hl' : 1 < ↑{ length := n + 1 + 1, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

Tactic:
·

Goal state after:
case mp.succ.zero
α : Type u_1
inst✝ : Preorder α
l : Fin (0 + 1 + 1) → α
hl : ∀ (i : Fin (0 + 1)), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
hl' : 1 < ↑{ length := 0 + 1, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b
Module: Mathlib.Order.KrullDimension

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

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝ : Preorder α
⊢ (∃ x, (∃ b, b < x) ∧ ∃ b, x < b) → ∃ i, 1 < ↑i.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝ : IsEmpty α
⊢ InfiniteDimensionalOrder α

pp: case inr
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝ : Nonempty α
⊢ InfiniteDimensionalOrder α

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝ : IsEmpty α
⊢ InfiniteDimensionalOrder α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ InfiniteDimensionalOrder α

pp: case inr.inr
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝¹ : Nonempty α
h✝ : InfiniteDimensionalOrder α
⊢ InfiniteDimensionalOrder α

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ InfiniteDimensionalOrder α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝¹ : Nonempty α
h✝ : InfiniteDimensionalOrder α
⊢ InfiniteDimensionalOrder α

Tactic:
·

Goal state after:
case inr.inr
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝¹ : Nonempty α
h✝ : InfiniteDimensionalOrder α
⊢ InfiniteDimensionalOrder α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝ : IsEmpty α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

pp: case inr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝ : Nonempty α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝ : IsEmpty α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

pp: case inr.inr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : InfiniteDimensionalOrder α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr.inl.mp
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ n ≤ (LTSeries.longestOf α).length → ∃ l, l.length = n

pp: case inr.inl.mpr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ (∃ l, l.length = n) → n ≤ (LTSeries.longestOf α).length

Tactic:
·

Goal state after:
case inr.inl.mp
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ n ≤ (LTSeries.longestOf α).length → ∃ l, l.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr.inl.mpr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ (∃ l, l.length = n) → n ≤ (LTSeries.longestOf α).length

Tactic:
·

Goal state after:
case inr.inl.mpr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ (∃ l, l.length = n) → n ≤ (LTSeries.longestOf α).length
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case refine_1
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
t : RelSeries {(a, b) | a ⋖ b}
i : Fin (s.length + 1) ↪ Fin (t.length + 1)
hit : t.toFun ∘ ⇑i = s.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last s.length) = Fin.last t.length
⊢ t.head = ⊥

pp: case refine_2
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
t : RelSeries {(a, b) | a ⋖ b}
i : Fin (s.length + 1) ↪ Fin (t.length + 1)
hit : t.toFun ∘ ⇑i = s.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last s.length) = Fin.last t.length
⊢ t.last = ⊤

Tactic:
·

Goal state after:
case refine_1
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
t : RelSeries {(a, b) | a ⋖ b}
i : Fin (s.length + 1) ↪ Fin (t.length + 1)
hit : t.toFun ∘ ⇑i = s.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last s.length) = Fin.last t.length
⊢ t.head = ⊥
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : InfiniteDimensionalOrder α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n

Tactic:
·

Goal state after:
case inr.inr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : InfiniteDimensionalOrder α
⊢ ↑n ≤ krullDim α ↔ ∃ l, l.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Preorder α
⊢ ⨆ p, ↑p.length < ↑↑0 ↔ ∀ (l : LTSeries α), l.length < 0

pp: case succ
α : Type u_1
inst✝ : Preorder α
n : ℕ
⊢ ⨆ p, ↑p.length < ↑↑(n + 1) ↔ ∀ (l : LTSeries α), l.length < n + 1

Tactic:
·

Goal state after:
case zero
α : Type u_1
inst✝ : Preorder α
⊢ ⨆ p, ↑p.length < ↑↑0 ↔ ∀ (l : LTSeries α), l.length < 0
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Preorder α
n : ℕ
⊢ ⨆ p, ↑p.length < ↑↑(n + 1) ↔ ∀ (l : LTSeries α), l.length < n + 1

Tactic:
·

Goal state after:
case succ
α : Type u_1
inst✝ : Preorder α
n : ℕ
⊢ ⨆ p, ↑p.length < ↑↑(n + 1) ↔ ∀ (l : LTSeries α), l.length < n + 1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
⊢ ↑(height (RelSeries.last (LTSeries.longestOf α))) = krullDim α

Tactic:
refine le_antisymm (height_le_krullDim _) ?_

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
⊢ krullDim α ≤ ↑(height (RelSeries.last (LTSeries.longestOf α)))
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case refine_2
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
t : RelSeries {(a, b) | a ⋖ b}
i : Fin (s.length + 1) ↪ Fin (t.length + 1)
hit : t.toFun ∘ ⇑i = s.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last s.length) = Fin.last t.length
⊢ t.last = ⊤

Tactic:
·

Goal state after:
case refine_2
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
t : RelSeries {(a, b) | a ⋖ b}
i : Fin (s.length + 1) ↪ Fin (t.length + 1)
hit : t.toFun ∘ ⇑i = s.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last s.length) = Fin.last t.length
⊢ t.last = ⊤
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α ≤ ↑(⨆ a, height a)

pp: case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(⨆ a, height a) ≤ krullDim α

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α ≤ ↑(⨆ a, height a)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(⨆ a, height a) ≤ krullDim α

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(⨆ a, height a) ≤ krullDim α