awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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)
have refine : some (some m) <
  (↑(RelSeries.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (LTSeries.withLength α (m + 1))) :
    WithBot ℕ∞)
Tactic: refine (not_lt_of_ge (hm (LTSeries.withLength _ (m + 1))) ?_).elim
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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) <
    (↑(RelSeries.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (LTSeries.withLength α (m + 1))) :
      WithBot ℕ∞)
have rw : m <
  (↑(RelSeries.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (LTSeries.withLength α (m + 1))) :
    ℕ)
Tactic: rw [WithBot.some_eq_coe, ← WithBot.coe_natCast, WithBot.coe_lt_coe,
      WithTop.some_eq_coe, ← WithTop.coe_natCast, WithTop.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ krullDim α = ⊤ ↔ InfiniteDimensionalOrder α
have refine : ∀ (h : krullDim α = ⊤), InfiniteDimensionalOrder α
Tactic: refine ⟨fun h ↦ ?_, fun _ ↦ krullDim_eq_top⟩
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
h : krullDim α = ⊤
⊢ InfiniteDimensionalOrder α
have inl : IsEmpty α → InfiniteDimensionalOrder α
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
h : krullDim α = ⊤
inl : IsEmpty α → InfiniteDimensionalOrder α
⊢ InfiniteDimensionalOrder α
have inr : Nonempty α → InfiniteDimensionalOrder α
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
h : krullDim α = ⊤
h_1 : Nonempty α
⊢ InfiniteDimensionalOrder α
have inr : FiniteDimensionalOrder α → InfiniteDimensionalOrder α
Tactic: cases finiteDimensionalOrder_or_infiniteDimensionalOrder α
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
h : krullDim α = ⊤
h_1 : Nonempty α
inr : FiniteDimensionalOrder α → InfiniteDimensionalOrder α
⊢ InfiniteDimensionalOrder α
have inr₁ : InfiniteDimensionalOrder α → InfiniteDimensionalOrder α
Tactic: cases finiteDimensionalOrder_or_infiniteDimensionalOrder α
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
h : krullDim α = ⊤
h_1 : Nonempty α
h_2 : FiniteDimensionalOrder α
⊢ InfiniteDimensionalOrder α
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
⊢ (↑n : WithBot ℕ∞) ≤ krullDim α ↔
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n
have inl : IsEmpty α →
  ((↑n : WithBot ℕ∞) ≤ krullDim α ↔
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n)
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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)
⊢ (↑n : WithBot ℕ∞) ≤ krullDim α ↔
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n
have inr : Nonempty α →
  ((↑n : WithBot ℕ∞) ≤ krullDim α ↔
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n)
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
h : Nonempty α
⊢ (↑n : WithBot ℕ∞) ≤ krullDim α ↔
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n
have inr : FiniteDimensionalOrder α →
  ((↑n : WithBot ℕ∞) ≤ krullDim α ↔
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n)
Tactic: cases finiteDimensionalOrder_or_infiniteDimensionalOrder α
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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)
⊢ (↑n : WithBot ℕ∞) ≤ krullDim α ↔
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n
have inr₁ : InfiniteDimensionalOrder α →
  ((↑n : WithBot ℕ∞) ≤ krullDim α ↔
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n)
Tactic: cases finiteDimensionalOrder_or_infiniteDimensionalOrder α
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
h : Nonempty α
h_1 : FiniteDimensionalOrder α
⊢ (↑n : WithBot ℕ∞) ≤ krullDim α ↔
    ∃ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n
have 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
Tactic: rw [krullDim_eq_length_of_finiteDimensionalOrder, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
h : Nonempty α
h_1 : FiniteDimensionalOrder α
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
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 ≤
      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
have inr₁ : (∃ (l : LTSeries α),
    l.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) =
      n) →
  n ≤
    RelSeries.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (LTSeries.longestOf α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
⊢ LT.lt (α := WithBot ℕ∞)
      (⨆ (p : LTSeries α),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          WithBot ℕ∞))
      (↑(↑n : ℕ∞) : WithBot ℕ∞) ↔
    ∀ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) <
        n
have zero : LT.lt (α := WithBot ℕ∞)
    (⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞))
    (↑(↑0 : ℕ∞) : WithBot ℕ∞) ↔
  ∀ (l : LTSeries α),
    l.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) <
      0
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
n : ℕ
zero :
  LT.lt (α := WithBot ℕ∞)
      (⨆ (p : LTSeries α),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          WithBot ℕ∞))
      (↑(↑0 : ℕ∞) : WithBot ℕ∞) ↔
    ∀ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) <
        0
⊢ LT.lt (α := WithBot ℕ∞)
      (⨆ (p : LTSeries α),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          WithBot ℕ∞))
      (↑(↑n : ℕ∞) : WithBot ℕ∞) ↔
    ∀ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) <
        n
have succ : ∀ (n : ℕ),
  LT.lt (α := WithBot ℕ∞)
      (⨆ (p : LTSeries α),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          WithBot ℕ∞))
      (↑(↑(n + 1) : ℕ∞) : WithBot ℕ∞) ↔
    ∀ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) <
        n + 1
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ LT.lt (α := WithBot ℕ∞)
      (⨆ (p : LTSeries α),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          WithBot ℕ∞))
      (↑(↑0 : ℕ∞) : WithBot ℕ∞) ↔
    ∀ (l : LTSeries α),
      l.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) <
        0
have zero : Eq (α := WithBot ℕ∞)
    (⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞))
    ⊥ ↔
  ∀ (l : LTSeries α),
    l.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) <
      0
Tactic: rw [ENat.coe_zero, ← bot_eq_zero, WithBot.lt_coe_bot]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ (↑(height a) : WithBot ℕ∞) ≤ krullDim α
have this : Nonempty α
Tactic: have : Nonempty α := ⟨a⟩
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
this : Nonempty α
⊢ (↑(height a) : WithBot ℕ∞) ≤ krullDim α
have rw : (↑(height a) : WithBot ℕ∞) ≤
  (↑(⨆ (p : LTSeries α),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)) :
    WithBot ℕ∞)
Tactic: rw [krullDim_eq_iSup_length]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
this : Nonempty α
⊢ (↑(height a) : WithBot ℕ∞) ≤
    (↑(⨆ (p : LTSeries α),
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞)) :
      WithBot ℕ∞)
have simp : height a ≤ ⨆ (p : LTSeries α), (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)
Tactic: simp only [WithBot.coe_le_coe]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
⊢ (↑(height
          (RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            (LTSeries.longestOf α))) :
      WithBot ℕ∞) =
    krullDim α
have refine : krullDim α ≤
  (↑(height
        (RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (LTSeries.longestOf α))) :
    WithBot ℕ∞)
Tactic: refine le_antisymm (height_le_krullDim _) ?_
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
⊢ krullDim α ≤
    (↑(height
          (RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            (LTSeries.longestOf α))) :
      WithBot ℕ∞)
have rw : LE.le (α := WithBot ℕ∞)
  (↑(RelSeries.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (LTSeries.longestOf α)) :
    WithBot ℕ∞)
  (↑(⨆ (p : LTSeries α),
        ⨆ (_ :
          RelSeries.last (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p ≤
            RelSeries.last (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              (LTSeries.longestOf α)),
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞)) :
    WithBot ℕ∞)
Tactic: rw [krullDim_eq_length_of_finiteDimensionalOrder, height]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
⊢ LE.le (α := WithBot ℕ∞)
    (↑(RelSeries.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (LTSeries.longestOf α)) :
      WithBot ℕ∞)
    (↑(⨆ (p : LTSeries α),
          ⨆ (_ :
            RelSeries.last (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                p ≤
              RelSeries.last (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                (LTSeries.longestOf α)),
            (↑(p.length (r :=
                  {x : α × α |
                    match (motive := α × α → Prop) x with
                    | (a, b) => a < b})) :
              ℕ∞)) :
      WithBot ℕ∞)
have norm_cast : LE.le (α := ℕ∞)
  (↑(RelSeries.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (LTSeries.longestOf α)) :
    ℕ∞)
  (⨆ (p : LTSeries α),
    ⨆ (_ :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p ≤
        RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (LTSeries.longestOf α)),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ krullDim α = (↑(⨆ (a : α), height a) : WithBot ℕ∞)
have a : krullDim α ≤ (↑(⨆ (a : α), height a) : WithBot ℕ∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
a : krullDim α ≤ (↑(⨆ (a : α), height a) : WithBot ℕ∞)
⊢ krullDim α = (↑(⨆ (a : α), height a) : WithBot ℕ∞)
have a₁ : (↑(⨆ (a : α), height a) : WithBot ℕ∞) ≤ krullDim α
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ krullDim α ≤ (↑(⨆ (a : α), height a) : WithBot ℕ∞)
have a : ∀ (i : LTSeries α),
  LE.le (α := WithBot ℕ∞)
    (↑(i.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      WithBot ℕ∞)
    (↑(⨆ (a : α), height a) : WithBot ℕ∞)
Tactic: apply iSup_le
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
p : LTSeries α
⊢ LE.le (α := WithBot ℕ∞)
    (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      WithBot ℕ∞)
    (↑(⨆ (a : α), height a) : WithBot ℕ∞)
have a : LE.le (α := ℕ∞)
  (↑(p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})) :
    ℕ∞)
  (⨆ (a : α), height a)
Tactic: suffices p.length ≤ ⨆ (a : α), height a from (WithBot.unbotD_le_iff fun _ => this).mp this
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ (↑(⨆ (a : α), height a) : WithBot ℕ∞) ≤ krullDim α
have a : ⨆ (i : α), (↑(height i) : WithBot ℕ∞) ≤ krullDim α
Tactic: rw [WithBot.coe_iSup (by bddDefault)]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ ⨆ (i : α), (↑(height i) : WithBot ℕ∞) ≤ krullDim α
have a : ∀ (i : α), (↑(height i) : WithBot ℕ∞) ≤ krullDim α
Tactic: apply iSup_le
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ krullDim α = (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞)
have a : krullDim α ≤ (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
a : krullDim α ≤ (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞)
⊢ krullDim α = (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞)
have a₁ : (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞) ≤ krullDim α
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ krullDim α ≤ (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞)
have a : LE.le (α := ℕ∞) (⨆ (a : α), height a) (⨆ (a : α), height a + coheight a)
Tactic: rw [krullDim_eq_iSup_height_of_nonempty, WithBot.coe_le_coe]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞) ≤ krullDim α
have a : ∀
  (this :
    ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α] (hnottop : krullDim α < ⊤),
      (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞) ≤ krullDim α)
  (hnottop : ¬krullDim α < ⊤), (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞) ≤ krullDim α
Tactic: wlog hnottop : krullDim α < ⊤
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
a :
  ∀
    (this :
      ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α] (hnottop : krullDim α < ⊤),
        (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞) ≤ krullDim α)
    (hnottop : ¬krullDim α < ⊤), (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞) ≤ krullDim α
⊢ (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞) ≤ krullDim α
have wlog : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α] (hnottop : krullDim α < ⊤),
  (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞) ≤ krullDim α
Tactic: wlog hnottop : krullDim α < ⊤
Cleared hypotheses: inst_1
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : Nonempty α
hnottop : krullDim α < ⊤
⊢ (↑(⨆ (a : α), height a + coheight a) : WithBot ℕ∞) ≤ krullDim α
have rw : LE.le (α := ℕ∞) (⨆ (a : α), height a + coheight a)
  (⨆ (p : LTSeries α),
    (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞))
Tactic: rw [krullDim_eq_iSup_length, WithBot.coe_le_coe]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : Nonempty α
hnottop : krullDim α < ⊤
⊢ LE.le (α := ℕ∞) (⨆ (a : α), height a + coheight a)
    (⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞))
have h : ∀ (i : α),
  height i + coheight i ≤
    ⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
Tactic: apply iSup_le
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : Nonempty α
hnottop : krullDim α < ⊤
a : α
⊢ height a + coheight a ≤
    ⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
have this : height a < ⊤
Tactic: have : height a < ⊤ := WithBot.coe_lt_coe.mp (lt_of_le_of_lt (height_le_krullDim a) hnottop)
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : Nonempty α
hnottop : krullDim α < ⊤
a : α
this : height a < ⊤
⊢ height a + coheight a ≤
    ⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
have this₁ : coheight a < ⊤
Tactic: have : coheight a < ⊤ := WithBot.coe_lt_coe.mp (lt_of_le_of_lt (coheight_le_krullDim a) hnottop)