awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
a : ∀ a < x, height a ≤ (↑n : ℕ∞) ↔ height a < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
⊢ ((∃ y < x, height y = (↑n : ℕ∞)) ∧ ∀ y < x, height y ≤ (↑n : ℕ∞)) ↔
    (∃ y < x, height y = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 - 1) ∧ ∀ y < x, height y < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1

Tactic:
congr! 3
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
h : y < x
a : LE.le (α := ℕ∞) ⊤ (↑n : ℕ∞) ↔ ⊤ < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
a₁ : ∀ (a : ℕ), LE.le (α := ℕ∞) (↑a : ℕ∞) (↑n : ℕ∞) ↔ (↑a : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
⊢ height y ≤ (↑n : ℕ∞) ↔ height y < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1

Tactic:
cases height y

Premises used: Order.height
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
h : y < x
⊢ LE.le (α := ℕ∞) ⊤ (↑n : ℕ∞) ↔ ⊤ < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
h : y < x
a_1 : ℕ
a : a_1 ≤ n ↔ (↑a_1 : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
⊢ LE.le (α := ℕ∞) (↑a_1 : ℕ∞) (↑n : ℕ∞) ↔ (↑a_1 : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
h : y < x
a_1 : ℕ
a : a_1 ≤ n ↔ a_1 < n + 1
⊢ a_1 ≤ n ↔ (↑a_1 : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1

Tactic:
norm_cast
-- Module: Mathlib.Order.KrullDimension
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
h : y < x
a : ℕ
⊢ a ≤ n ↔ a < n + 1

Tactic:
lia
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
n : ℕ
⊢ coheight x = (↑n : ℕ∞) ↔
    coheight x < ⊤ ∧ (n = 0 ∨ ∃ y > x, coheight y = HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1) ∧ ∀ y > x, coheight y < (↑n : ℕ∞)

Tactic:
height_eq_coe_iff (α := αᵒᵈ)

Premises used: Order.height_eq_coe_iff, OrderDual, Order.coheight
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
pos : ∀ (hfin : height a < ⊤), height a = (↑n : ℕ∞) ↔ Minimal (fun (y : α) ↦ (↑n : ℕ∞) ≤ height y) a
neg : ∀ (hfin : ⊤ ≤ height a), height a = (↑n : ℕ∞) ↔ Minimal (fun (y : α) ↦ (↑n : ℕ∞) ≤ height y) a
⊢ height a = (↑n : ℕ∞) ↔ Minimal (fun (y : α) ↦ (↑n : ℕ∞) ≤ height y) a

Tactic:
by_cases! hfin : height a < ⊤

Premises used: Order.height
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
hfin : height a < ⊤
hn : n = 0
⊢ height a = (↑0 : ℕ∞) ↔ Minimal (fun (y : α) ↦ (↑0 : ℕ∞) ≤ height y) a

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
hfin : height a < ⊤
n_1 : ℕ
hn : n = n_1 + 1
⊢ height a = (↑(n_1 + 1) : ℕ∞) ↔ Minimal (fun (y : α) ↦ (↑(n_1 + 1) : ℕ∞) ≤ height y) a

Tactic:
simp [minimal_iff_forall_lt, height_eq_coe_add_one_iff, ENat.add_one_le_iff,
        coe_lt_height_iff, *]

Premises used: ENat.add_one_le_iff, Order.height_eq_coe_add_one_iff, minimal_iff_forall_lt, Order.coe_lt_height_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
hfin : height a < ⊤
pos : ∀ (x : ℕ) (hn : n = x), height a = (↑x : ℕ∞) ↔ Minimal (fun (y : α) ↦ (↑x : ℕ∞) ≤ height y) a
⊢ height a = (↑n : ℕ∞) ↔ Minimal (fun (y : α) ↦ (↑n : ℕ∞) ≤ height y) a

Tactic:
cases hn : n with
    | zero => simp
    | succ => simp [minimal_iff_forall_lt, height_eq_coe_add_one_iff, ENat.add_one_le_iff,
        coe_lt_height_iff, *]

Premises used: Order.succ, ENat.add_one_le_iff, Order.height_eq_coe_add_one_iff, minimal_iff_forall_lt, Order.coe_lt_height_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
hfin : ⊤ ≤ height a
this : ∃ x < a, (↑n : ℕ∞) ≤ height x
⊢ height a = (↑n : ℕ∞) ↔ Minimal (fun (y : α) ↦ (↑n : ℕ∞) ≤ height y) a

Tactic:
simp_all [minimal_iff_forall_lt]

Premises used: minimal_iff_forall_lt
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
hfin : ⊤ ≤ height a
neg : ∃ x < a, (↑n : ℕ∞) ≤ height x
⊢ height a = (↑n : ℕ∞) ↔ Minimal (fun (y : α) ↦ (↑n : ℕ∞) ≤ height y) a

Tactic:
suffices ∃ x < a, ↑n ≤ height x by
      simp_all [minimal_iff_forall_lt]
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
hfin : ⊤ ≤ height a
⊢ ∀ (n : ℕ),
    ∃ (p : LTSeries α),
      RelSeries.last (r := {x : α × α | x.1 < x.2}) p = a ∧ p.length (r := {x : α × α | x.1 < x.2}) = n

Tactic:
simp only [top_le_iff, height_eq_top_iff] at hfin

Premises used: top_le_iff, Order.height_eq_top_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
hfin :
  ∀ (n : ℕ),
    ∃ (p : LTSeries α),
      RelSeries.last (r := {x : α × α | x.1 < x.2}) p = a ∧ p.length (r := {x : α × α | x.1 < x.2}) = n
neg :
  ∀ (p : LTSeries α) (hp : p.length (r := {x : α × α | x.1 < x.2}) = n + 1)
    (hfin :
      ∀ (n : ℕ),
        ∃ (p_1 : LTSeries α),
          RelSeries.last (r := {x : α × α | x.1 < x.2}) p_1 = RelSeries.last (r := {x : α × α | x.1 < x.2}) p ∧
            p_1.length (r := {x : α × α | x.1 < x.2}) = n),
    ∃ x < RelSeries.last (r := {x : α × α | x.1 < x.2}) p, (↑n : ℕ∞) ≤ height x
⊢ ∃ x < a, (↑n : ℕ∞) ≤ height x

Tactic:
obtain ⟨p, rfl, hp⟩ := hfin (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
p : LTSeries α
hp : p.length (r := {x : α × α | x.1 < x.2}) = n + 1
hfin :
  ∀ (n : ℕ),
    ∃ (p_1 : LTSeries α),
      RelSeries.last (r := {x : α × α | x.1 < x.2}) p_1 = RelSeries.last (r := {x : α × α | x.1 < x.2}) p ∧
        p_1.length (r := {x : α × α | x.1 < x.2}) = n
⊢ p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) ≠
    0

Tactic:
lia
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
p : LTSeries α
hp : p.length (r := {x : α × α | x.1 < x.2}) = n + 1
hfin :
  ∀ (n : ℕ),
    ∃ (p_1 : LTSeries α),
      RelSeries.last (r := {x : α × α | x.1 < x.2}) p_1 = RelSeries.last (r := {x : α × α | x.1 < x.2}) p ∧
        p_1.length (r := {x : α × α | x.1 < x.2}) = n
right :
  (↑n : ℕ∞) ≤
    height
      ((RelSeries.eraseLast (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p).last
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}))
⊢ ∃ x < RelSeries.last (r := {x : α × α | x.1 < x.2}) p, (↑n : ℕ∞) ≤ height x

Tactic:
use p.eraseLast.last, p.eraseLast_last_rel_last (by lia)

Premises used: RelSeries.last, RelSeries.eraseLast, RelSeries.eraseLast_last_rel_last
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
p : LTSeries α
hp : p.length (r := {x : α × α | x.1 < x.2}) = n + 1
hfin :
  ∀ (n : ℕ),
    ∃ (p_1 : LTSeries α),
      RelSeries.last (r := {x : α × α | x.1 < x.2}) p_1 = RelSeries.last (r := {x : α × α | x.1 < x.2}) p ∧
        p_1.length (r := {x : α × α | x.1 < x.2}) = n
⊢ (↑n : ℕ∞) ≤
    height
      ((RelSeries.eraseLast (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p).last
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}))

Tactic:
simpa [hp] using length_le_height_last (p := p.eraseLast)

Premises used: Order.length_le_height_last
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
⊢ coheight a = (↑n : ℕ∞) ↔ Maximal (fun (y : α) ↦ (↑n : ℕ∞) ≤ coheight y) a

Tactic:
height_eq_coe_iff_minimal_le_height (α := αᵒᵈ)

Premises used: Maximal, OrderDual, Order.height_eq_coe_iff_minimal_le_height, Order.coheight
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
rw : 2 ≤ height x ↔ ∃ (y : α), ∃ z < y, y < x
⊢ 1 < height x ↔ ∃ (y : α), ∃ z < y, y < x

Tactic:
rw [← ENat.add_one_le_iff ENat.one_ne_top, one_add_one_eq_two]

Premises used: ENat.one_ne_top, ENat.add_one_le_iff, one_add_one_eq_two
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ 2 ≤ height x ↔ ∃ (y : α), ∃ z < y, y < x

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
refine_1 : ∀ (h : 2 ≤ height x), ∃ (y : α), ∃ z < y, y < x
refine_2 : (∃ (y : α), ∃ z < y, y < x) → 2 ≤ height x
⊢ 2 ≤ height x ↔ ∃ (y : α), ∃ z < y, y < x

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
h : 2 ≤ height x
refine_1 :
  ∀ (p : LTSeries α)
    (hp :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        x)
    (hlen :
      p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        2),
    ∃ (y : α), ∃ z < y, y < x
⊢ ∃ (y : α), ∃ z < y, y < x

Tactic:
obtain ⟨p, hp, hlen⟩ := Order.exists_series_of_le_height x (n := 2) h

Premises used: Order.exists_series_of_le_height
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
h : 2 ≤ height x
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    2
⊢ ∃ (y : α), ∃ z < y, y < x

Tactic:
⟨p 1, p 0, p.rel_of_lt ?_, hp ▸ p.rel_of_lt ?_⟩

Premises used: Eq.rec, And.intro, Exists.intro, RelSeries.toFun, RelSeries.rel_of_lt, OfNat.ofNat
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
h : 2 ≤ height x
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    2
refine_1 :
  LT.lt (α :=
    Fin
      (p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) +
        1))
    0 1
refine_1₁ :
  LT.lt (α :=
    Fin
      (p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) +
        1))
    1
    (Fin.last
      (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})))
⊢ ∃ (y : α), ∃ z < y, y < x

Tactic:
refine ⟨p 1, p 0, p.rel_of_lt ?_, hp ▸ p.rel_of_lt ?_⟩
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
h : 2 ≤ height x
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    2
⊢ LT.lt (α :=
    Fin
      (p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) +
        1))
    0 1

Tactic:
simp [Fin.lt_def, hlen]

Premises used: Fin.lt_def
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x : α
h : 2 ≤ height x
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
hlen :
  p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    2
⊢ LT.lt (α :=
    Fin
      (p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) +
        1))
    1
    (Fin.last
      (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})))

Tactic:
simp [Fin.lt_def, hlen]

Premises used: Fin.lt_def
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x y z : α
hzy : z < y
hyx : y < x
p : LTSeries α :=
  RelSeries.fromListIsChain (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    [z, y, x] ⋯ ⋯
⊢ RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x

Tactic:
simp [p, ← RelSeries.getLast_toList]

Premises used: RelSeries.getLast_toList
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x y z : α
hzy : z < y
hyx : y < x
p : LTSeries α :=
  RelSeries.fromListIsChain (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    [z, y, x] ⋯ ⋯
⊢ RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x

Tactic:
have : p.last = x := by simp [p, ← RelSeries.getLast_toList]
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x y z : α
hzy : z < y
hyx : y < x
p : LTSeries α :=
  RelSeries.fromListIsChain (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    [z, y, x] ⋯ ⋯
this :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
⊢ 2 ≤ height x

Tactic:
Order.length_le_height this.le

Premises used: Eq.le, Order.length_le_height, Nat.pred
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x y z : α
hzy : z < y
hyx : y < x
p : LTSeries α :=
  RelSeries.fromListIsChain (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    [z, y, x] ⋯ ⋯
this :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p =
    x
⊢ 2 ≤ height x

Tactic:
exact Order.length_le_height this.le

Premises used: Eq.le, Order.length_le_height
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
p : LTSeries α
⊢ (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      WithBot ℕ∞) ≤
    krullDim α

Tactic:
le_sSup ⟨_, rfl⟩

Premises used: iSup, Order.krullDim, Exists.intro, le_sSup, rfl
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
rw :
  (∀ (i : LTSeries α),
      LE.le (α := WithBot ℕ∞)
        (↑(i.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          WithBot ℕ∞)
        ⊥) ↔
    IsEmpty α
⊢ krullDim α = ⊥ ↔ IsEmpty α

Tactic:
rw [eq_bot_iff, krullDim, iSup_le_iff]

Premises used: Order.krullDim, iSup_le_iff, eq_bot_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
simp : (∀ (i : LTSeries α), False) ↔ ∀ (a : α), False
⊢ (∀ (i : LTSeries α),
      LE.le (α := WithBot ℕ∞)
        (↑(i.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          WithBot ℕ∞)
        ⊥) ↔
    IsEmpty α

Tactic:
simp only [le_bot_iff, WithBot.natCast_ne_bot, isEmpty_iff]

Premises used: le_bot_iff, isEmpty_iff, WithBot.natCast_ne_bot
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
H : ∀ (i : LTSeries α), False
x : α
⊢ ∀ (i : Fin 0),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      ((fun (x_1 : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ x) i.castSucc, (fun (x_1 : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ x) i.succ)

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
⊢ (∀ (i : LTSeries α), False) ↔ ∀ (a : α), False

Tactic:
exact ⟨fun H x ↦ H ⟨0, fun _ ↦ x, by simp⟩, (· <| · 1)⟩
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
contrapose! : krullDim α < 0 ↔ IsEmpty α
⊢ 0 ≤ krullDim α ↔ Nonempty α

Tactic:
contrapose!
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
rw : krullDim α < 0 ↔ krullDim α = ⊥
rw₁ : krullDim α < 0 ↔ krullDim α < (↑⊥ : WithBot ℕ∞)
rw₂ : krullDim α < 0 ↔ krullDim α < (↑0 : WithBot ℕ∞)
rw₃ rw₄ : krullDim α < 0 ↔ krullDim α < 0
⊢ krullDim α < 0 ↔ IsEmpty α

Tactic:
rw [← krullDim_eq_bot_iff, ← WithBot.lt_coe_bot, bot_eq_zero, WithBot.coe_zero]

Premises used: Order.krullDim_eq_bot_iff, WithBot.lt_coe_bot, bot_eq_zero, WithBot.coe_zero
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : IsEmpty α
⊢ krullDim α = ⊥

Tactic:
krullDim_eq_bot_iff.mpr ‹_›

Premises used: Iff.mpr, Order.krullDim_eq_bot_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ 0 ≤ krullDim α

Tactic:
krullDim_nonneg_iff.mpr ‹_›

Premises used: Iff.mpr, Order.krullDim_nonneg_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
rw : ¬krullDim α = ⊥ ↔ Nonempty α
rw₁ : ¬IsEmpty α ↔ Nonempty α
rw₂ rw₃ : Nonempty α ↔ Nonempty α
⊢ krullDim α ≠ ⊥ ↔ Nonempty α

Tactic:
rw [ne_eq, krullDim_eq_bot_iff, not_isEmpty_iff]

Premises used: ne_eq, Order.krullDim_eq_bot_iff, not_isEmpty_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
rw : krullDim α ≠ ⊥ ↔ Nonempty α
rw₁ rw₂ : Nonempty α ↔ Nonempty α
⊢ ⊥ < krullDim α ↔ Nonempty α

Tactic:
rw [bot_lt_iff_ne_bot, krullDim_ne_bot_iff]

Premises used: Order.krullDim_ne_bot_iff, bot_lt_iff_ne_bot
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ ⊥ < krullDim α

Tactic:
bot_lt_krullDim_iff.mpr ‹_›

Premises used: Iff.mpr, Order.bot_lt_krullDim_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
simp :
  (∀ (i : LTSeries α), LE.le (α := WithBot ℕ∞) (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞) 0) ↔
    ∀ (x b : α), ¬x < b
⊢ krullDim α ≤ 0 ↔ ∀ (x : α), IsMax x

Tactic:
simp only [krullDim, iSup_le_iff, isMax_iff_forall_not_lt]

Premises used: Order.krullDim, isMax_iff_forall_not_lt, iSup_le_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
H : ∀ (i : LTSeries α), LE.le (α := WithBot ℕ∞) (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞) 0
x y : α
h : x < y
i : Fin 1
obtain :
  Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (![x, y] (Fin.castSucc 0), ![x, y] (Fin.succ 0))
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (![x, y] i.castSucc, ![x, y] i.succ)

Tactic:
obtain rfl := Subsingleton.elim i 0

Premises used: Subsingleton.elim, OfNat.ofNat, rfl
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
H : ∀ (i : LTSeries α), LE.le (α := WithBot ℕ∞) (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞) 0
x y : α
h : x < y
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (![x, y] (Fin.castSucc 0), ![x, y] (Fin.succ 0))

Tactic:
simpa
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
H : ∀ (i : LTSeries α), LE.le (α := WithBot ℕ∞) (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞) 0
x y : α
h : x < y
⊢ LT.lt (α := WithBot ℕ∞) 0
    (↑(RelSeries.length (r := {x : α × α | x.1 < x.2})
          (RelSeries.mk (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            1 ![x, y] ⋯)) :
      WithBot ℕ∞)

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
refine :
  (∀ (x b : α), ¬x < b) →
    ∀ (i : LTSeries α), LE.le (α := WithBot ℕ∞) (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞) 0
⊢ (∀ (i : LTSeries α), LE.le (α := WithBot ℕ∞) (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞) 0) ↔
    ∀ (x b : α), ¬x < b

Tactic:
refine ⟨fun H x y h ↦ (H ⟨1, ![x, y],
    fun i ↦ by obtain rfl := Subsingleton.elim i 0; simpa⟩).not_gt (by simp), ?_⟩
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
H : ∀ (x b : α), ¬x < b
l : Fin (HAdd.hAdd (α := ℕ) 0 1) → α
h :
  ∀ (i : Fin 0),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (l i.castSucc, l i.succ)
⊢ LE.le (α := WithBot ℕ∞)
    (↑((RelSeries.mk (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              0 l h).length
          (r := {x : α × α | x.1 < x.2})) :
      WithBot ℕ∞)
    0

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
H : ∀ (x b : α), ¬x < b
n : ℕ
l : Fin (n + 1 + 1) → α
h :
  ∀ (i : Fin (n + 1)),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (l i.castSucc, l i.succ)
⊢ LE.le (α := WithBot ℕ∞)
    (↑((RelSeries.mk (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              (n + 1) l h).length
          (r := {x : α × α | x.1 < x.2})) :
      WithBot ℕ∞)
    0

Tactic:
cases H (l 0) (l 1) (h 0)

Premises used: OfNat.ofNat
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
simp : (∀ (x : α) ⦃b : α⦄, x ≤ b → b ≤ x) ↔ ∀ (x : α) ⦃b : α⦄, b ≤ x → x ≤ b
⊢ krullDim α ≤ 0 ↔ ∀ (x : α), IsMin x

Tactic:
simp only [krullDim_nonpos_iff_forall_isMax, IsMax, IsMin]

Premises used: Order.krullDim_nonpos_iff_forall_isMax, IsMin, IsMax
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
⊢ (∀ (x : α) ⦃b : α⦄, x ≤ b → b ≤ x) ↔ ∀ (x : α) ⦃b : α⦄, b ≤ x → x ≤ b

Tactic:
forall_comm

Premises used: forall_comm
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
⊢ (∀ (x : α) ⦃b : α⦄, x ≤ b → b ≤ x) ↔ ∀ (x : α) ⦃b : α⦄, b ≤ x → x ≤ b

Tactic:
exact forall_comm

Premises used: forall_comm
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
simp_rw :
  (∀ (i : LTSeries α), LE.le (α := WithBot ℕ∞) (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞) 1) ↔
    ∀ (x : α), (∀ (b : α), ¬b < x) ∨ ∀ (b : α), ¬x < b
⊢ krullDim α ≤ 1 ↔ ∀ (x : α), IsMin x ∨ IsMax x

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

Premises used: Order.krullDim, isMax_iff_forall_not_lt, isMin_iff_forall_not_lt, iSup_le_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
contrapose! :
  (∃ (i : LTSeries α), LT.lt (α := WithBot ℕ∞) 1 (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞)) ↔
    ∃ (x : α), (∃ (b : α), b < x) ∧ ∃ (b : α), x < b
⊢ (∀ (i : LTSeries α), LE.le (α := WithBot ℕ∞) (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞) 1) ↔
    ∀ (x : α), (∀ (b : α), ¬b < x) ∨ ∀ (b : α), ¬x < b

Tactic:
contrapose!
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
mp :
  (∃ (i : LTSeries α), LT.lt (α := WithBot ℕ∞) 1 (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞)) →
    ∃ (x : α), (∃ (b : α), b < x) ∧ ∃ (b : α), x < b
mpr :
  (∃ (x : α), (∃ (b : α), b < x) ∧ ∃ (b : α), x < b) →
    ∃ (i : LTSeries α), LT.lt (α := WithBot ℕ∞) 1 (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞)
⊢ (∃ (i : LTSeries α), LT.lt (α := WithBot ℕ∞) 1 (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞)) ↔
    ∃ (x : α), (∃ (b : α), b < x) ∧ ∃ (b : α), x < b

Tactic:
constructor