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 α
inst_2 : Nonempty α
hnottop : krullDim α < ⊤
a : α
this_1 : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = (↑n : ℕ∞)
m : ℕ
hch : coheight a = (↑m : ℕ∞)
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) (↑m : ℕ∞) ≤
    ⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
have h : ∀ (p₁ : LTSeries α)
  (hlast :
    RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p₁ =
      a)
  (hlen₁ :
    p₁.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) =
      n),
  HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) (↑m : ℕ∞) ≤
    ⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
Tactic: obtain ⟨p₁, hlast, hlen₁⟩ := exists_series_of_height_eq_coe a hh
-- 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 : α
this_1 : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = (↑n : ℕ∞)
m : ℕ
hch : coheight a = (↑m : ℕ∞)
p₁ : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p₁ =
    a
hlen₁ :
  p₁.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) =
    n
⊢ HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) (↑m : ℕ∞) ≤
    ⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
have h : ∀ (p₂ : LTSeries α)
  (hhead :
    RelSeries.head (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p₂ =
      a)
  (hlen₂ :
    p₂.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) =
      m),
  HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) (↑m : ℕ∞) ≤
    ⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
Tactic: obtain ⟨p₂, hhead, hlen₂⟩ := exists_series_of_coheight_eq_coe a hch
-- 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 : α
this_1 : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = (↑n : ℕ∞)
⊢ (↑n : ℕ∞) + coheight a ≤
    ⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
have h : ∀ (x : ℕ∞) (hch : coheight a = x),
  (↑n : ℕ∞) + x ≤
    ⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
Tactic: cases hch : coheight a with
      | top => simp_all
      | coe m =>
        obtain ⟨p₁, hlast, hlen₁⟩ := exists_series_of_height_eq_coe a hh
        obtain ⟨p₂, hhead, hlen₂⟩ := exists_series_of_coheight_eq_coe a hch
        apply le_iSup_of_le ((p₁.smash p₂) (by simp [*])) (by simp [*])
-- 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 : α
this_1 : height a < ⊤
this : coheight a < ⊤
⊢ height a + coheight a ≤
    ⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
have h : ∀ (x : ℕ∞) (hh : height a = x),
  x + coheight a ≤
    ⨆ (p : LTSeries α),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
Tactic: cases hh : height a with
    | top => simp_all
    | coe n =>
      cases hch : coheight a with
      | top => simp_all
      | coe m =>
        obtain ⟨p₁, hlast, hlen₁⟩ := exists_series_of_height_eq_coe a hh
        obtain ⟨p₂, hhead, hlen₂⟩ := exists_series_of_coheight_eq_coe a hch
        apply le_iSup_of_le ((p₁.smash p₂) (by simp [*])) (by simp [*])
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
h : IsEmpty α
⊢ krullDim α = ⨆ (a : α), (↑(height a) : WithBot ℕ∞)
have inl : Eq (α := WithBot ℕ∞) ⊥ (⨆ (a : α), (↑(height a) : WithBot ℕ∞))
Tactic: rw [krullDim_eq_bot, ciSup_of_empty]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
h : IsEmpty α
inl : Eq (α := WithBot ℕ∞) ⊥ (⨆ (a : α), (↑(height a) : WithBot ℕ∞))
⊢ krullDim α = ⨆ (a : α), (↑(height a) : WithBot ℕ∞)
have inl₁ : Eq (α := WithBot ℕ∞) ⊥ ⊥
Tactic: rw [krullDim_eq_bot, ciSup_of_empty]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
h : Nonempty α
⊢ krullDim α = ⨆ (a : α), (↑(height a) : WithBot ℕ∞)
have inr : Eq (α := WithBot ℕ∞) (↑(⨆ (a : α), height a) : WithBot ℕ∞) (⨆ (a : α), (↑(height a) : WithBot ℕ∞))
Tactic: rw [krullDim_eq_iSup_height_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
h : Nonempty α
inr : Eq (α := WithBot ℕ∞) (↑(⨆ (a : α), height a) : WithBot ℕ∞) (⨆ (a : α), (↑(height a) : WithBot ℕ∞))
⊢ krullDim α = ⨆ (a : α), (↑(height a) : WithBot ℕ∞)
have inr₁ : Eq (α := WithBot ℕ∞) (⨆ (i : α), (↑(height i) : WithBot ℕ∞)) (⨆ (a : α), (↑(height a) : WithBot ℕ∞))
Tactic: rw [krullDim_eq_iSup_height_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
⊢ krullDim α = ⨆ (a : α), (↑(height a) : WithBot ℕ∞)
have x : IsEmpty α ∨ Nonempty α
Tactic: cases isEmpty_or_nonempty α with
  | inl h => rw [krullDim_eq_bot, ciSup_of_empty]
  | inr h => rw [krullDim_eq_iSup_height_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
h : IsEmpty α
⊢ krullDim α = ⨆ (a : α), (↑(coheight a) : WithBot ℕ∞)
have inl : Eq (α := WithBot ℕ∞) ⊥ (⨆ (a : α), (↑(coheight a) : WithBot ℕ∞))
Tactic: rw [krullDim_eq_bot, ciSup_of_empty]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
h : IsEmpty α
inl : Eq (α := WithBot ℕ∞) ⊥ (⨆ (a : α), (↑(coheight a) : WithBot ℕ∞))
⊢ krullDim α = ⨆ (a : α), (↑(coheight a) : WithBot ℕ∞)
have inl₁ : Eq (α := WithBot ℕ∞) ⊥ ⊥
Tactic: rw [krullDim_eq_bot, ciSup_of_empty]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
h : Nonempty α
⊢ krullDim α = ⨆ (a : α), (↑(coheight a) : WithBot ℕ∞)
have inr : Eq (α := WithBot ℕ∞) (↑(⨆ (a : α), coheight a) : WithBot ℕ∞) (⨆ (a : α), (↑(coheight a) : WithBot ℕ∞))
Tactic: rw [krullDim_eq_iSup_coheight_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
h : Nonempty α
inr : Eq (α := WithBot ℕ∞) (↑(⨆ (a : α), coheight a) : WithBot ℕ∞) (⨆ (a : α), (↑(coheight a) : WithBot ℕ∞))
⊢ krullDim α = ⨆ (a : α), (↑(coheight a) : WithBot ℕ∞)
have inr₁ : Eq (α := WithBot ℕ∞) (⨆ (i : α), (↑(coheight i) : WithBot ℕ∞)) (⨆ (a : α), (↑(coheight a) : WithBot ℕ∞))
Tactic: rw [krullDim_eq_iSup_coheight_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
⊢ krullDim α = ⨆ (a : α), (↑(coheight a) : WithBot ℕ∞)
have x : IsEmpty α ∨ Nonempty α
Tactic: cases isEmpty_or_nonempty α with
  | inl h => rw [krullDim_eq_bot, ciSup_of_empty]
  | inr h => rw [krullDim_eq_iSup_coheight_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
⊢ (↑(height.{u_1} (α := α) ⊤) : WithBot ℕ∞) = krullDim α
have rw : (↑(height.{u_1} (α := α) ⊤) : 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 α
inst_1 : OrderTop α
⊢ (↑(height.{u_1} (α := α) ⊤) : WithBot ℕ∞) =
    (↑(⨆ (p : LTSeries α),
          (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞)) :
      WithBot ℕ∞)
have simp : height.{u_1} (α := α) ⊤ = ⨆ (p : LTSeries α), (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)
Tactic: simp only [WithBot.coe_inj]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
⊢ height.{u_1} (α := α) ⊤ = ⨆ (p : LTSeries α), (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)
have a : height.{u_1} (α := α) ⊤ ≤ ⨆ (p : LTSeries α), (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
a : height.{u_1} (α := α) ⊤ ≤ ⨆ (p : LTSeries α), (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)
⊢ height.{u_1} (α := α) ⊤ = ⨆ (p : LTSeries α), (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)
have a₁ : ⨆ (p : LTSeries α), (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞) ≤ height.{u_1} (α := α) ⊤
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
⊢ (↑(coheight.{u_1} (α := α) ⊥) : WithBot ℕ∞) = krullDim α
have rw : (↑(coheight.{u_1} (α := α) ⊥) : WithBot ℕ∞) = krullDim.{u_1} αᵒᵈ
Tactic: rw [← krullDim_orderDual]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ (↑(height x) : WithBot ℕ∞) = krullDim.{u_1} (↑(Set.Iic x) : Type u_1)
have rw : Eq (α := ℕ∞)
  (⨆ (p : LTSeries α),
    ⨆ (_ :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p ≤
        x),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞))
  (⨆ (p : LTSeries (↑(Set.Iic x) : Type u_1)),
    ⨆ (_ :
      RelSeries.last (r :=
          {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
            match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
            | (a, b) => a < b})
          p ≤
        ⊤),
      (↑(p.length (r :=
            {x_2 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
              match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_2 with
              | (a, b) => a < b})) :
        ℕ∞))
Tactic: rw [← height_top_eq_krullDim, height, height, WithBot.coe_inj]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ Eq (α := ℕ∞)
    (⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p ≤
          x),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞))
    (⨆ (p : LTSeries (↑(Set.Iic x) : Type u_1)),
      ⨆ (_ :
        RelSeries.last (r :=
            {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
              match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
              | (a, b) => a < b})
            p ≤
          ⊤),
        (↑(p.length (r :=
              {x_2 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
                match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_2 with
                | (a, b) => a < b})) :
          ℕ∞))
have a : LE.le (α := ℕ∞)
  (⨆ (p : LTSeries α),
    ⨆ (_ :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p ≤
        x),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞))
  (⨆ (p : LTSeries (↑(Set.Iic x) : Type u_1)),
    ⨆ (_ :
      RelSeries.last (r :=
          {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
            match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
            | (a, b) => a < b})
          p ≤
        ⊤),
      (↑(p.length (r :=
            {x_2 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
              match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_2 with
              | (a, b) => a < b})) :
        ℕ∞))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
a :
  LE.le (α := ℕ∞)
    (⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p ≤
          x),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞))
    (⨆ (p : LTSeries (↑(Set.Iic x) : Type u_1)),
      ⨆ (_ :
        RelSeries.last (r :=
            {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
              match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
              | (a, b) => a < b})
            p ≤
          ⊤),
        (↑(p.length (r :=
              {x_2 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
                match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_2 with
                | (a, b) => a < b})) :
          ℕ∞))
⊢ Eq (α := ℕ∞)
    (⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p ≤
          x),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞))
    (⨆ (p : LTSeries (↑(Set.Iic x) : Type u_1)),
      ⨆ (_ :
        RelSeries.last (r :=
            {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
              match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
              | (a, b) => a < b})
            p ≤
          ⊤),
        (↑(p.length (r :=
              {x_2 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
                match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_2 with
                | (a, b) => a < b})) :
          ℕ∞))
have a₁ : LE.le (α := ℕ∞)
  (⨆ (p : LTSeries (↑(Set.Iic x) : Type u_1)),
    ⨆ (_ :
      RelSeries.last (r :=
          {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
            match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
            | (a, b) => a < b})
          p ≤
        ⊤),
      (↑(p.length (r :=
            {x_2 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
              match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_2 with
              | (a, b) => a < b})) :
        ℕ∞))
  (⨆ (p : LTSeries α),
    ⨆ (_ :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p ≤
        x),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ LE.le (α := ℕ∞)
    (⨆ (p : LTSeries α),
      ⨆ (_ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p ≤
          x),
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞))
    (⨆ (p : LTSeries (↑(Set.Iic x) : Type u_1)),
      ⨆ (_ :
        RelSeries.last (r :=
            {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
              match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
              | (a, b) => a < b})
            p ≤
          ⊤),
        (↑(p.length (r :=
              {x_2 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
                match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_2 with
                | (a, b) => a < b})) :
          ℕ∞))
have a : ∀ (i : LTSeries α),
  LE.le (α := ℕ∞)
    (⨆ (_ :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i ≤
        x),
      (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞))
    (⨆ (p : LTSeries (↑(Set.Iic x) : Type u_1)),
      ⨆ (_ :
        RelSeries.last (r :=
            {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
              match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
              | (a, b) => a < b})
            p ≤
          ⊤),
        (↑(p.length (r :=
              {x_2 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
                match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_2 with
                | (a, b) => a < b})) :
          ℕ∞))
Tactic: apply iSup_le
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries α
⊢ LE.le (α := ℕ∞)
    (⨆ (_ :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p ≤
        x),
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞))
    (⨆ (p : LTSeries (↑(Set.Iic x) : Type u_1)),
      ⨆ (_ :
        RelSeries.last (r :=
            {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
              match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
              | (a, b) => a < b})
            p ≤
          ⊤),
        (↑(p.length (r :=
              {x_2 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
                match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_2 with
                | (a, b) => a < b})) :
          ℕ∞))
have a : ∀
  (i :
    RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p ≤
      x),
  LE.le (α := ℕ∞)
    (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
    (⨆ (p : LTSeries (↑(Set.Iic x) : Type u_1)),
      ⨆ (_ :
        RelSeries.last (r :=
            {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
              match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
              | (a, b) => a < b})
            p ≤
          ⊤),
        (↑(p.length (r :=
              {x_2 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
                match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_2 with
                | (a, b) => a < b})) :
          ℕ∞))
Tactic: apply iSup_le
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
q : LTSeries { x_1 : α // x_1 ∈ Set.Iic x } :=
  LTSeries.mk
    (p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}))
    (fun
        (i :
          Fin
            (p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) +
              1)) ↦
      Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Set.Iic x)
        (p.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i)
        ⋯)
    ⋯
⊢ LE.le (α := ℕ∞)
    (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
    (⨆ (p : LTSeries (↑(Set.Iic x) : Type u_1)),
      ⨆ (_ :
        RelSeries.last (r :=
            {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
              match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_1 with
              | (a, b) => a < b})
            p ≤
          ⊤),
        (↑(p.length (r :=
              {x_2 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) |
                match (motive := (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) → Prop) x_2 with
                | (a, b) => a < b})) :
          ℕ∞))
have a : LE.le (α := ℕ∞) (↑(p.length (r := {x : α × α | x.1 < x.2})) : ℕ∞)
  (⨆ (p : LTSeries (↑(Set.Iic x) : Type u_1)),
    (↑(p.length (r := {x_1 : (↑(Set.Iic x) : Type u_1) × (↑(Set.Iic x) : Type u_1) | x_1.1 < x_1.2})) : ℕ∞))
Tactic: simp only [le_top, iSup_pos, ge_iff_le]