awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
l : Fin (HAdd.hAdd (α := ℕ) 0 1) → α
hl :
  ∀ (i : Fin 0),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (l i.castSucc, l i.succ)
hl' :
  LT.lt (α := WithBot ℕ∞) 1
    (↑((RelSeries.mk (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              0 l hl).length
          (r := {x : α × α | x.1 < x.2})) :
      WithBot ℕ∞)
⊢ LE.le (α := WithBot ℕ∞)
    (↑((RelSeries.mk (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              0 l hl).length
          (r := {x : α × α | x.1 < x.2})) :
      WithBot ℕ∞)
    1

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
l : Fin (HAdd.hAdd (α := ℕ) 0 1) → α
hl :
  ∀ (i : Fin 0),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (l i.castSucc, l i.succ)
hl' :
  LT.lt (α := WithBot ℕ∞) 1
    (↑((RelSeries.mk (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              0 l hl).length
          (r := {x : α × α | x.1 < x.2})) :
      WithBot ℕ∞)
⊢ ∃ (x : α), (∃ (b : α), b < x) ∧ ∃ (b : α), x < b

Tactic:
cases hl'.not_ge (by simp)

Premises used: LT.lt.not_ge
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
l : Fin (HAdd.hAdd (α := ℕ) 0 1 + 1) → α
hl :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (l i.castSucc, l i.succ)
hl' :
  LT.lt (α := WithBot ℕ∞) 1
    (↑((RelSeries.mk (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              (HAdd.hAdd (α := ℕ) 0 1) l hl).length
          (r := {x : α × α | x.1 < x.2})) :
      WithBot ℕ∞)
⊢ LE.le (α := WithBot ℕ∞)
    (↑((RelSeries.mk (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              (HAdd.hAdd (α := ℕ) 0 1) l hl).length
          (r := {x : α × α | x.1 < x.2})) :
      WithBot ℕ∞)
    1

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

Tactic:
cases hl'.not_ge (by simp)

Premises used: LT.lt.not_ge
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
l : Fin (n + 1 + 1 + 1) → α
hl :
  ∀ (i : Fin (n + 1 + 1)),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (l i.castSucc, l i.succ)
hl' :
  LT.lt (α := WithBot ℕ∞) 1
    (↑((RelSeries.mk (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              (n + 1 + 1) l hl).length
          (r := {x : α × α | x.1 < x.2})) :
      WithBot ℕ∞)
⊢ ∃ (x : α), (∃ (b : α), b < x) ∧ ∃ (b : α), x < b

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

Premises used: And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
l : Fin (n + 1 + 1 + 1) → α
hl :
  ∀ (i : Fin (n + 1 + 1)),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (l i.castSucc, l i.succ)
hl' :
  LT.lt (α := WithBot ℕ∞) 1
    (↑((RelSeries.mk (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              (n + 1 + 1) l hl).length
          (r := {x : α × α | x.1 < x.2})) :
      WithBot ℕ∞)
⊢ ∃ (x : α), (∃ (b : α), b < x) ∧ ∃ (b : α), x < b

Tactic:
exact ⟨l 1, ⟨l 0, hl 0⟩, l 2, hl 1⟩
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x y : α
hxy : y < x
z : α
hzx : x < z
i : Fin 2
0 :
  Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (![y, x, z] (Fin.castSucc ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))),
      ![y, x, z] (Fin.succ ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))))
1 :
  Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (![y, x, z] (Fin.castSucc ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))),
      ![y, x, z] (Fin.succ ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))))
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (![y, x, z] i.castSucc, ![y, x, z] i.succ)

Tactic:
fin_cases i
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x y : α
hxy : y < x
z : α
hzx : x < z
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (![y, x, z] (Fin.castSucc ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))),
      ![y, x, z] (Fin.succ ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))))

Tactic:
simpa
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x y : α
hxy : y < x
z : α
hzx : x < z
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (![y, x, z] (Fin.castSucc ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))),
      ![y, x, z] (Fin.succ ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))))

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

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
x y : α
hxy : y < x
z : α
hzx : x < z
⊢ ∃ (i : LTSeries α), LT.lt (α := WithBot ℕ∞) 1 (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞)

Tactic:
exact ⟨⟨2, ![y, x, z], fun i ↦ by fin_cases i <;> simpa⟩, by simp⟩
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
contrapose! : krullDim α ≤ 0 ↔ ∀ (x y : α), ¬x < y
⊢ 0 < krullDim α ↔ ∃ (x : α) (y : α), x < y

Tactic:
contrapose!
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
simp_rw : krullDim α ≤ 0 ↔ ∀ (x : α), IsMax x
⊢ krullDim α ≤ 0 ↔ ∀ (x y : α), ¬x < y

Tactic:
simp_rw [← isMax_iff_forall_not_lt, ← krullDim_nonpos_iff_forall_isMax]

Premises used: Order.krullDim_nonpos_iff_forall_isMax, isMax_iff_forall_not_lt
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
rw : 1 ≤ krullDim α ↔ 0 < krullDim α
rw₁ : 1 ≤ krullDim α ↔ (↑0 : WithBot ℕ∞) < krullDim α
rw₂ : 1 ≤ krullDim α ↔ HAdd.hAdd (α := WithBot ℕ∞) (↑0 : WithBot ℕ∞) 1 ≤ krullDim α
rw₃ : 1 ≤ krullDim α ↔ HAdd.hAdd (α := WithBot ℕ∞) 0 1 ≤ krullDim α
rw₄ rw₅ : 1 ≤ krullDim α ↔ 1 ≤ krullDim α
⊢ 1 ≤ krullDim α ↔ ∃ (x : α) (y : α), x < y

Tactic:
rw [← krullDim_pos_iff, ← Nat.cast_zero, ← ENat.WithBot.add_one_le_iff, Nat.cast_zero, zero_add]

Premises used: Order.krullDim_pos_iff, zero_add, ENat.WithBot.add_one_le_iff, Nat.cast_zero
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Subsingleton α
rw : ∀ (x : α), IsMax x
⊢ krullDim α ≤ 0

Tactic:
rw [krullDim_nonpos_iff_forall_isMax]

Premises used: Order.krullDim_nonpos_iff_forall_isMax
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Subsingleton α
⊢ ∀ (x : α), IsMax x

Tactic:
fun x y h ↦ (Subsingleton.elim x y).ge

Premises used: Eq.ge, Subsingleton.elim, IsMax
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Subsingleton α
⊢ ∀ (x : α), IsMax x

Tactic:
exact fun x y h ↦ (Subsingleton.elim x y).ge

Premises used: Eq.ge, Subsingleton.elim
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Subsingleton α
⊢ krullDim α = 0

Tactic:
le_antisymm krullDim_nonpos_of_subsingleton krullDim_nonneg

Premises used: Order.krullDim_nonpos_of_subsingleton, le_antisymm, Order.krullDim_nonneg
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Unique α
⊢ krullDim α = 0

Tactic:
le_antisymm krullDim_nonpos_of_subsingleton krullDim_nonneg

Premises used: Order.krullDim_nonpos_of_subsingleton, le_antisymm, Order.krullDim_nonneg
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : OrderBot α
⊢ krullDim α ≤ 1 ↔ ∀ (x : α), x ≠ ⊥ → IsMax x

Tactic:
simp [krullDim_le_one_iff, ← or_iff_not_imp_left]

Premises used: Order.krullDim_le_one_iff, Classical.or_iff_not_imp_left
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : OrderBot α
⊢ krullDim α = 0 ↔ Subsingleton α

Tactic:
⟨fun H ↦ subsingleton_of_forall_eq ⊥ fun _ ↦ le_bot_iff.mp
    (krullDim_nonpos_iff_forall_isMax.mp H.le ⊥ bot_le), fun _ ↦ Order.krullDim_eq_zero⟩

Premises used: le_bot_iff, subsingleton_of_forall_eq, Order.krullDim_nonpos_iff_forall_isMax, Eq.le, Bot.bot, Iff.intro, Iff.mp, Order.krullDim_eq_zero, bot_le
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : OrderBot α
rw : ¬krullDim α < 0
⊢ 0 < krullDim α ↔ Nontrivial α

Tactic:
rw [← not_subsingleton_iff_nontrivial, ← Order.krullDim_eq_zero_iff_of_orderBot,
    ← ne_eq, ← lt_or_lt_iff_ne, or_iff_right]

Premises used: ne_eq, or_iff_right, not_subsingleton_iff_nontrivial, lt_or_lt_iff_ne, Order.krullDim_eq_zero_iff_of_orderBot
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : OrderBot α
⊢ ¬krullDim α < 0

Tactic:
simp [Order.krullDim_nonneg]

Premises used: Order.krullDim_nonneg
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
⊢ krullDim α ≤ 1 ↔ ∀ (x : α), x ≠ ⊤ → IsMin x

Tactic:
simp [krullDim_le_one_iff, ← or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right, Order.krullDim_le_one_iff
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
⊢ krullDim α = 0 ↔ Subsingleton α

Tactic:
⟨fun H ↦ subsingleton_of_forall_eq ⊤ fun _ ↦ top_le_iff.mp
    (krullDim_nonpos_iff_forall_isMin.mp H.le ⊤ le_top), fun _ ↦ Order.krullDim_eq_zero⟩

Premises used: subsingleton_of_forall_eq, Order.krullDim_nonpos_iff_forall_isMin, Eq.le, le_top, Iff.intro, top_le_iff, Iff.mp, Order.krullDim_eq_zero, Top.top
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
rw : ¬krullDim α < 0
⊢ 0 < krullDim α ↔ Nontrivial α

Tactic:
rw [← not_subsingleton_iff_nontrivial, ← Order.krullDim_eq_zero_iff_of_orderTop,
    ← ne_eq, ← lt_or_lt_iff_ne, or_iff_right]

Premises used: ne_eq, Order.krullDim_eq_zero_iff_of_orderTop, or_iff_right, not_subsingleton_iff_nontrivial, lt_or_lt_iff_ne
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
⊢ ¬krullDim α < 0

Tactic:
simp [Order.krullDim_nonneg]

Premises used: Order.krullDim_nonneg
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : BoundedOrder α
⊢ krullDim α ≤ 1 ↔ ∀ (x : α), x = ⊥ ∨ x = ⊤

Tactic:
simp [Order.krullDim_le_one_iff]

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

Tactic:
le_antisymm
    (iSup_le <| fun _ ↦ WithBot.coe_le_coe.mpr <| WithTop.coe_le_coe.mpr <|
      RelSeries.length_le_length_longestOf _ _) <|
    le_iSup (fun (i : LTSeries _) ↦ (i.length : WithBot (WithTop ℕ))) <| LTSeries.longestOf _

Premises used: Iff.mpr, LTSeries.longestOf, setOf, FiniteDimensionalOrder.match_1, le_iSup, RelSeries.length, Nat.cast, WithBot.coe_le_coe, le_antisymm, LT.lt, iSup_le, RelSeries.length_le_length_longestOf, WithTop.coe_le_coe
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfiniteDimensionalOrder α
m : WithBot ℕ∞
hm_1 :
  ∀ (i : LTSeries α),
    (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      m
hm :
  ∀ (i : LTSeries α),
    LE.le (α := WithBot ℕ∞)
      (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞)
      ⊥
haveI : ∀ (this : Inhabited α), False
⊢ False

Tactic:
haveI : Inhabited α := ⟨LTSeries.withLength _ 0 0⟩
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfiniteDimensionalOrder α
m : WithBot ℕ∞
hm_1 :
  ∀ (i : LTSeries α),
    (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      m
hm :
  ∀ (i : LTSeries α),
    LE.le (α := WithBot ℕ∞)
      (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞)
      ⊥
this : Inhabited α
⊢ False

Tactic:
not_le_of_gt (WithBot.bot_lt_coe _ : ⊥ < (0 : WithBot (WithTop ℕ))) <| hm default

Premises used: Inhabited.default, WithBot.bot_lt_coe, not_le_of_gt
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfiniteDimensionalOrder α
m : WithBot ℕ∞
hm_1 :
  ∀ (i : LTSeries α),
    (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      m
hm :
  ∀ (i : LTSeries α),
    LE.le (α := WithBot ℕ∞)
      (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞)
      ⊥
this : Inhabited α
⊢ False

Tactic:
exact not_le_of_gt (WithBot.bot_lt_coe _ : ⊥ < (0 : WithBot (WithTop ℕ))) <| hm default

Premises used: Inhabited.default, WithBot.bot_lt_coe, not_le_of_gt
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfiniteDimensionalOrder α
m_1 : WithBot ℕ∞
hm_1 :
  ∀ (i : LTSeries α),
    (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      m_1
m : ℕ
hm :
  ∀ (i : LTSeries α),
    (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      some (some m)
⊢ ⊤ ≤ some (some m)

Tactic:
(not_lt_of_ge (hm (LTSeries.withLength _ (m + 1))) ?_).elim

Premises used: False.elim, HAdd.hAdd, LTSeries.withLength, OfNat.ofNat, not_lt_of_ge
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfiniteDimensionalOrder α
m_1 : WithBot ℕ∞
hm_1 :
  ∀ (i : LTSeries α),
    (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      m_1
m : ℕ
hm :
  ∀ (i : LTSeries α),
    (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      some (some m)
refine :
  some (some m) <
    (↑(RelSeries.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (LTSeries.withLength α (m + 1))) :
      WithBot ℕ∞)
⊢ ⊤ ≤ some (some m)

Tactic:
refine (not_lt_of_ge (hm (LTSeries.withLength _ (m + 1))) ?_).elim

Premises used: False.elim, HAdd.hAdd, LTSeries.withLength, OfNat.ofNat, not_lt_of_ge
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfiniteDimensionalOrder α
m_1 : WithBot ℕ∞
hm_1 :
  ∀ (i : LTSeries α),
    (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      m_1
m : ℕ
hm :
  ∀ (i : LTSeries α),
    (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      some (some m)
rw :
  m <
    (↑(RelSeries.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (LTSeries.withLength α (m + 1))) :
      ℕ)
⊢ some (some m) <
    (↑(RelSeries.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (LTSeries.withLength α (m + 1))) :
      WithBot ℕ∞)

Tactic:
rw [WithBot.some_eq_coe, ← WithBot.coe_natCast, WithBot.coe_lt_coe,
      WithTop.some_eq_coe, ← WithTop.coe_natCast, WithTop.coe_lt_coe]

Premises used: WithTop.coe_lt_coe, WithBot.coe_lt_coe, WithBot.some_eq_coe, WithTop.some_eq_coe, WithTop.coe_natCast, WithBot.coe_natCast
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfiniteDimensionalOrder α
m_1 : WithBot ℕ∞
hm_1 :
  ∀ (i : LTSeries α),
    (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      m_1
m : ℕ
hm :
  ∀ (i : LTSeries α),
    (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      some (some m)
⊢ m <
    (↑(RelSeries.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (LTSeries.withLength α (m + 1))) :
      ℕ)

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
⊢ krullDim α = ⊤ ↔ InfiniteDimensionalOrder α

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

Premises used: Order.krullDim_eq_top, Iff.intro
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
refine : ∀ (h : krullDim α = ⊤), InfiniteDimensionalOrder α
⊢ krullDim α = ⊤ ↔ InfiniteDimensionalOrder α

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ krullDim_eq_top⟩
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
h : krullDim α = ⊤
inl : IsEmpty α → InfiniteDimensionalOrder α
inr : Nonempty α → InfiniteDimensionalOrder α
⊢ InfiniteDimensionalOrder α

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
h : krullDim α = ⊤
h_1 : IsEmpty α
⊢ InfiniteDimensionalOrder α

Tactic:
simp [krullDim_eq_bot] at h

Premises used: Order.krullDim_eq_bot
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
h : krullDim α = ⊤
h_1 : Nonempty α
inr : FiniteDimensionalOrder α → InfiniteDimensionalOrder α
inr₁ : InfiniteDimensionalOrder α → InfiniteDimensionalOrder α
⊢ InfiniteDimensionalOrder α

Tactic:
cases finiteDimensionalOrder_or_infiniteDimensionalOrder α

Premises used: finiteDimensionalOrder_or_infiniteDimensionalOrder
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
h : krullDim α = ⊤
h_1 : Nonempty α
h_2 : FiniteDimensionalOrder α
⊢ Eq (α := WithBot ℕ∞)
    (↑(RelSeries.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (LTSeries.longestOf α)) :
      WithBot ℕ∞)
    ⊤

Tactic:
rw [krullDim_eq_length_of_finiteDimensionalOrder] at h

Premises used: Order.krullDim_eq_length_of_finiteDimensionalOrder
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
h_1 : Nonempty α
h_2 : FiniteDimensionalOrder α
h :
  Eq (α := WithBot ℕ∞)
    (↑(RelSeries.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (LTSeries.longestOf α)) :
      WithBot ℕ∞)
    ⊤
⊢ InfiniteDimensionalOrder α

Tactic:
cases h
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
h : krullDim α = ⊤
h_1 : Nonempty α
h_2 : InfiniteDimensionalOrder α
⊢ InfiniteDimensionalOrder α

Tactic:
infer_instance
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
inl :
  IsEmpty α →
    ((↑n : WithBot ℕ∞) ≤ krullDim α ↔
      ∃ (l : LTSeries α),
        l.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) =
          n)
inr :
  Nonempty α →
    ((↑n : WithBot ℕ∞) ≤ krullDim α ↔
      ∃ (l : LTSeries α),
        l.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) =
          n)
⊢ (↑n : WithBot ℕ∞) ≤ krullDim α ↔
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
h : IsEmpty α
⊢ (↑n : WithBot ℕ∞) ≤ krullDim α ↔
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n

Tactic:
simp [krullDim_eq_bot]

Premises used: Order.krullDim_eq_bot
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
h : Nonempty α
inr :
  FiniteDimensionalOrder α →
    ((↑n : WithBot ℕ∞) ≤ krullDim α ↔
      ∃ (l : LTSeries α),
        l.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) =
          n)
inr₁ :
  InfiniteDimensionalOrder α →
    ((↑n : WithBot ℕ∞) ≤ krullDim α ↔
      ∃ (l : LTSeries α),
        l.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) =
          n)
⊢ (↑n : WithBot ℕ∞) ≤ krullDim α ↔
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n

Tactic:
cases finiteDimensionalOrder_or_infiniteDimensionalOrder α

Premises used: finiteDimensionalOrder_or_infiniteDimensionalOrder
-- Module: Mathlib.Order.KrullDimension
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
h : Nonempty α
h_1 : FiniteDimensionalOrder α
inr :
  n ≤
      RelSeries.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (LTSeries.longestOf α) ↔
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n
⊢ (↑n : WithBot ℕ∞) ≤ krullDim α ↔
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n

Tactic:
rw [krullDim_eq_length_of_finiteDimensionalOrder, Nat.cast_le]

Premises used: Order.krullDim_eq_length_of_finiteDimensionalOrder, Nat.cast_le