awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
⊢ height x = (↑(n + 1) : ℕ∞) ↔
    (n + 1 = 0 ∨ ∃ y < x, height y = HSub.hSub (α := ℕ∞) (↑(n + 1) : ℕ∞) 1) ∧ ∀ y < x, height y < (↑(n + 1) : ℕ∞)
have simp : height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
  (∃ y < x, height y = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 - 1) ∧ ∀ y < x, height y < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
Tactic: simp only [Nat.cast_add, Nat.cast_one, add_eq_zero, one_ne_zero, and_false, false_or]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
⊢ height x = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ↔
    (∃ y < x, height y = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 - 1) ∧ ∀ y < x, height y < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
have rw : (height x < ⊤ ∧ (∃ 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: rw [height_eq_coe_add_one_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
⊢ (height x < ⊤ ∧ (∃ 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
have simp : ((∃ 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: simp only [hfin, true_and]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
⊢ ((∃ 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
have a : ∀ a < x, height a ≤ (↑n : ℕ∞) ↔ height a < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
Tactic: congr! 3
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
y : α
h : y < x
⊢ height y ≤ (↑n : ℕ∞) ↔ height y < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
have a : LE.le (α := ℕ∞) ⊤ (↑n : ℕ∞) ↔ ⊤ < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
Tactic: cases height y
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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
⊢ height y ≤ (↑n : ℕ∞) ↔ height y < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
have a₁ : ∀ (a : ℕ), LE.le (α := ℕ∞) (↑a : ℕ∞) (↑n : ℕ∞) ↔ (↑a : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
Tactic: cases height y
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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 (α := ℕ∞) (↑a : ℕ∞) (↑n : ℕ∞) ↔ (↑a : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
have a : a ≤ n ↔ (↑a : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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 : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
have a : a ≤ n ↔ a < n + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
⊢ height a = (↑n : ℕ∞) ↔ Minimal (fun (y : α) ↦ (↑n : ℕ∞) ≤ height y) a
have pos : ∀ (hfin : height a < ⊤), height a = (↑n : ℕ∞) ↔ Minimal (fun (y : α) ↦ (↑n : ℕ∞) ≤ height y) a
Tactic: by_cases! hfin : height a < ⊤
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
pos : ∀ (hfin : height a < ⊤), height a = (↑n : ℕ∞) ↔ Minimal (fun (y : α) ↦ (↑n : ℕ∞) ≤ height y) a
⊢ height a = (↑n : ℕ∞) ↔ Minimal (fun (y : α) ↦ (↑n : ℕ∞) ≤ height y) a
have neg : ∀ (hfin : ⊤ ≤ height a), height a = (↑n : ℕ∞) ↔ Minimal (fun (y : α) ↦ (↑n : ℕ∞) ≤ height y) a
Tactic: by_cases! hfin : height a < ⊤
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
hfin : height a < ⊤
⊢ height a = (↑n : ℕ∞) ↔ Minimal (fun (y : α) ↦ (↑n : ℕ∞) ≤ height y) a
have pos : ∀ (x : ℕ) (hn : n = x), height a = (↑x : ℕ∞) ↔ Minimal (fun (y : α) ↦ (↑x : ℕ∞) ≤ 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, *]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
hfin : ⊤ ≤ height a
⊢ height a = (↑n : ℕ∞) ↔ Minimal (fun (y : α) ↦ (↑n : ℕ∞) ≤ height y) a
have neg : ∃ x < a, (↑n : ℕ∞) ≤ height x
Tactic: suffices ∃ x < a, ↑n ≤ height x by
      simp_all [minimal_iff_forall_lt]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ
hfin : ⊤ ≤ height a
⊢ ∃ x < a, (↑n : ℕ∞) ≤ height x
have hfin₁ : ∀ (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
Cleared hypotheses: hfin
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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
⊢ ∃ x < a, (↑n : ℕ∞) ≤ height x
have 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
Tactic: obtain ⟨p, rfl, hp⟩ := hfin (n + 1)
Cleared hypotheses: a, hfin
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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
⊢ ∃ x < RelSeries.last (r := {x : α × α | x.1 < x.2}) p, (↑n : ℕ∞) ≤ height x
have 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}))
Tactic: use p.eraseLast.last, p.eraseLast_last_rel_last (by lia)
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ 1 < height x ↔ ∃ (y : α), ∃ z < y, y < x
have rw : 2 ≤ height x ↔ ∃ (y : α), ∃ z < y, y < x
Tactic: rw [← ENat.add_one_le_iff ENat.one_ne_top, one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ 2 ≤ height x ↔ ∃ (y : α), ∃ z < y, y < x
have refine_1 : ∀ (h : 2 ≤ height x), ∃ (y : α), ∃ z < y, y < x
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
refine_1 : ∀ (h : 2 ≤ height x), ∃ (y : α), ∃ z < y, y < x
⊢ 2 ≤ height x ↔ ∃ (y : α), ∃ z < y, y < x
have refine_2 : (∃ (y : α), ∃ z < y, y < x) → 2 ≤ height x
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
h : 2 ≤ height x
⊢ ∃ (y : α), ∃ z < y, y < x
have 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
Tactic: obtain ⟨p, hp, hlen⟩ := Order.exists_series_of_le_height x (n := 2) h
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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
have refine_1 : LT.lt (α :=
  Fin
    (p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1))
  0 1
Tactic: refine ⟨p 1, p 0, p.rel_of_lt ?_, hp ▸ p.rel_of_lt ?_⟩
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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
⊢ ∃ (y : α), ∃ z < y, y < x
have 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})))
Tactic: refine ⟨p 1, p 0, p.rel_of_lt ?_, hp ▸ p.rel_of_lt ?_⟩
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
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] ⋯ ⋯
⊢ 2 ≤ height x
have this : 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]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ krullDim α = ⊥ ↔ IsEmpty α
have rw : (∀ (i : LTSeries α),
    LE.le (α := WithBot ℕ∞)
      (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞)
      ⊥) ↔
  IsEmpty α
Tactic: rw [eq_bot_iff, krullDim, iSup_le_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ (∀ (i : LTSeries α),
      LE.le (α := WithBot ℕ∞)
        (↑(i.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          WithBot ℕ∞)
        ⊥) ↔
    IsEmpty α
have simp : (∀ (i : LTSeries α), False) ↔ ∀ (a : α), False
Tactic: simp only [le_bot_iff, WithBot.natCast_ne_bot, isEmpty_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ 0 ≤ krullDim α ↔ Nonempty α
have contrapose! : krullDim α < 0 ↔ IsEmpty α
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ krullDim α < 0 ↔ IsEmpty α
have rw : krullDim α < 0 ↔ krullDim α = ⊥
Tactic: rw [← krullDim_eq_bot_iff, ← WithBot.lt_coe_bot, bot_eq_zero, WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
rw : krullDim α < 0 ↔ krullDim α = ⊥
⊢ krullDim α < 0 ↔ IsEmpty α
have rw₁ : krullDim α < 0 ↔ krullDim α < (↑⊥ : WithBot ℕ∞)
Tactic: rw [← krullDim_eq_bot_iff, ← WithBot.lt_coe_bot, bot_eq_zero, WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
rw : krullDim α < 0 ↔ krullDim α = ⊥
rw₁ : krullDim α < 0 ↔ krullDim α < (↑⊥ : WithBot ℕ∞)
⊢ krullDim α < 0 ↔ IsEmpty α
have rw₂ : krullDim α < 0 ↔ krullDim α < (↑0 : WithBot ℕ∞)
Tactic: rw [← krullDim_eq_bot_iff, ← WithBot.lt_coe_bot, bot_eq_zero, WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
rw : krullDim α < 0 ↔ krullDim α = ⊥
rw₁ : krullDim α < 0 ↔ krullDim α < (↑⊥ : WithBot ℕ∞)
rw₂ : krullDim α < 0 ↔ krullDim α < (↑0 : WithBot ℕ∞)
⊢ krullDim α < 0 ↔ IsEmpty α
have rw₃ : krullDim α < 0 ↔ krullDim α < 0
Tactic: rw [← krullDim_eq_bot_iff, ← WithBot.lt_coe_bot, bot_eq_zero, WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ krullDim α ≠ ⊥ ↔ Nonempty α
have rw : ¬krullDim α = ⊥ ↔ Nonempty α
Tactic: rw [ne_eq, krullDim_eq_bot_iff, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
rw : ¬krullDim α = ⊥ ↔ Nonempty α
⊢ krullDim α ≠ ⊥ ↔ Nonempty α
have rw₁ : ¬IsEmpty α ↔ Nonempty α
Tactic: rw [ne_eq, krullDim_eq_bot_iff, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
rw : ¬krullDim α = ⊥ ↔ Nonempty α
rw₁ : ¬IsEmpty α ↔ Nonempty α
⊢ krullDim α ≠ ⊥ ↔ Nonempty α
have rw₂ : Nonempty α ↔ Nonempty α
Tactic: rw [ne_eq, krullDim_eq_bot_iff, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ ⊥ < krullDim α ↔ Nonempty α
have rw : krullDim α ≠ ⊥ ↔ Nonempty α
Tactic: rw [bot_lt_iff_ne_bot, krullDim_ne_bot_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
rw : krullDim α ≠ ⊥ ↔ Nonempty α
⊢ ⊥ < krullDim α ↔ Nonempty α
have rw₁ : Nonempty α ↔ Nonempty α
Tactic: rw [bot_lt_iff_ne_bot, krullDim_ne_bot_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ krullDim α ≤ 0 ↔ ∀ (x : α), IsMax x
have simp : (∀ (i : LTSeries α), LE.le (α := WithBot ℕ∞) (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞) 0) ↔
  ∀ (x b : α), ¬x < b
Tactic: simp only [krullDim, iSup_le_iff, isMax_iff_forall_not_lt]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (![x, y] i.castSucc, ![x, y] i.succ)
have obtain : Membership.mem (γ := SetRel α α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a < b}
  (![x, y] (Fin.castSucc 0), ![x, y] (Fin.succ 0))
Tactic: obtain rfl := Subsingleton.elim i 0
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ (∀ (i : LTSeries α), LE.le (α := WithBot ℕ∞) (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞) 0) ↔
    ∀ (x b : α), ¬x < b
have refine : (∀ (x b : α), ¬x < b) →
  ∀ (i : LTSeries α), LE.le (α := WithBot ℕ∞) (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞) 0
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), ?_⟩
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ krullDim α ≤ 0 ↔ ∀ (x : α), IsMin x
have simp : (∀ (x : α) ⦃b : α⦄, x ≤ b → b ≤ x) ↔ ∀ (x : α) ⦃b : α⦄, b ≤ x → x ≤ b
Tactic: simp only [krullDim_nonpos_iff_forall_isMax, IsMax, IsMin]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ krullDim α ≤ 1 ↔ ∀ (x : α), IsMin x ∨ IsMax x
have simp_rw : (∀ (i : LTSeries α), LE.le (α := WithBot ℕ∞) (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞) 1) ↔
  ∀ (x : α), (∀ (b : α), ¬b < x) ∨ ∀ (b : α), ¬x < b
Tactic: simp_rw [isMax_iff_forall_not_lt, isMin_iff_forall_not_lt, krullDim, iSup_le_iff]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ (∀ (i : LTSeries α), LE.le (α := WithBot ℕ∞) (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞) 1) ↔
    ∀ (x : α), (∀ (b : α), ¬b < x) ∨ ∀ (b : α), ¬x < b
have contrapose! : (∃ (i : LTSeries α), LT.lt (α := WithBot ℕ∞) 1 (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞)) ↔
  ∃ (x : α), (∃ (b : α), b < x) ∧ ∃ (b : α), x < b
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ (∃ (i : LTSeries α), LT.lt (α := WithBot ℕ∞) 1 (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞)) ↔
    ∃ (x : α), (∃ (b : α), b < x) ∧ ∃ (b : α), x < b
have mp : (∃ (i : LTSeries α), LT.lt (α := WithBot ℕ∞) 1 (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞)) →
  ∃ (x : α), (∃ (b : α), b < x) ∧ ∃ (b : α), x < b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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
⊢ (∃ (i : LTSeries α), LT.lt (α := WithBot ℕ∞) 1 (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞)) ↔
    ∃ (x : α), (∃ (b : α), b < x) ∧ ∃ (b : α), x < b
have mpr : (∃ (x : α), (∃ (b : α), b < x) ∧ ∃ (b : α), x < b) →
  ∃ (i : LTSeries α), LT.lt (α := WithBot ℕ∞) 1 (↑(i.length (r := {x : α × α | x.1 < x.2})) : WithBot ℕ∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x y : α
hxy : y < x
z : α
hzx : x < z
i : 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)
have 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, sorry⟩ : Fin 2))),
    ![y, x, z] (Fin.succ ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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))))
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (![y, x, z] i.castSucc, ![y, x, z] i.succ)
have 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, sorry⟩ : Fin 2))),
    ![y, x, z] (Fin.succ ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ 0 < krullDim α ↔ ∃ (x : α) (y : α), x < y
have contrapose! : krullDim α ≤ 0 ↔ ∀ (x y : α), ¬x < y
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ krullDim α ≤ 0 ↔ ∀ (x y : α), ¬x < y
have simp_rw : krullDim α ≤ 0 ↔ ∀ (x : α), IsMax x
Tactic: simp_rw [← isMax_iff_forall_not_lt, ← krullDim_nonpos_iff_forall_isMax]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ 1 ≤ krullDim α ↔ ∃ (x : α) (y : α), x < y
have rw : 1 ≤ krullDim α ↔ 0 < krullDim α
Tactic: rw [← krullDim_pos_iff, ← Nat.cast_zero, ← ENat.WithBot.add_one_le_iff, Nat.cast_zero, zero_add]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
rw : 1 ≤ krullDim α ↔ 0 < krullDim α
⊢ 1 ≤ krullDim α ↔ ∃ (x : α) (y : α), x < y
have rw₁ : 1 ≤ krullDim α ↔ (↑0 : WithBot ℕ∞) < krullDim α
Tactic: rw [← krullDim_pos_iff, ← Nat.cast_zero, ← ENat.WithBot.add_one_le_iff, Nat.cast_zero, zero_add]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
rw : 1 ≤ krullDim α ↔ 0 < krullDim α
rw₁ : 1 ≤ krullDim α ↔ (↑0 : WithBot ℕ∞) < krullDim α
⊢ 1 ≤ krullDim α ↔ ∃ (x : α) (y : α), x < y
have rw₂ : 1 ≤ krullDim α ↔ HAdd.hAdd (α := WithBot ℕ∞) (↑0 : WithBot ℕ∞) 1 ≤ krullDim α
Tactic: rw [← krullDim_pos_iff, ← Nat.cast_zero, ← ENat.WithBot.add_one_le_iff, Nat.cast_zero, zero_add]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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 α
⊢ 1 ≤ krullDim α ↔ ∃ (x : α) (y : α), x < y
have rw₃ : 1 ≤ krullDim α ↔ HAdd.hAdd (α := WithBot ℕ∞) 0 1 ≤ krullDim α
Tactic: rw [← krullDim_pos_iff, ← Nat.cast_zero, ← ENat.WithBot.add_one_le_iff, Nat.cast_zero, zero_add]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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 α
⊢ 1 ≤ krullDim α ↔ ∃ (x : α) (y : α), x < y
have rw₄ : 1 ≤ krullDim α ↔ 1 ≤ krullDim α
Tactic: rw [← krullDim_pos_iff, ← Nat.cast_zero, ← ENat.WithBot.add_one_le_iff, Nat.cast_zero, zero_add]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Subsingleton α
⊢ krullDim α ≤ 0
have rw : ∀ (x : α), IsMax x
Tactic: rw [krullDim_nonpos_iff_forall_isMax]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : OrderBot α
⊢ 0 < krullDim α ↔ Nontrivial α
have rw : ¬krullDim α < 0
Tactic: rw [← not_subsingleton_iff_nontrivial, ← Order.krullDim_eq_zero_iff_of_orderBot,
    ← ne_eq, ← lt_or_lt_iff_ne, or_iff_right]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
⊢ 0 < krullDim α ↔ Nontrivial α
have rw : ¬krullDim α < 0
Tactic: rw [← not_subsingleton_iff_nontrivial, ← Order.krullDim_eq_zero_iff_of_orderTop,
    ← ne_eq, ← lt_or_lt_iff_ne, or_iff_right]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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 ℕ∞)
      ⊥
⊢ False
have haveI : ∀ (this : Inhabited α), False
Tactic: haveI : Inhabited α := ⟨LTSeries.withLength _ 0 0⟩