awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ 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})) :
          ℕ∞))
have a : ∀ (i : LTSeries (↑(Set.Iic x) : Type u_1)),
  LE.le (α := ℕ∞)
    (⨆ (_ :
      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})
          i ≤
        ⊤),
      (↑(i.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 iSup_le
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (↑(Set.Iic x) : Type u_1)
⊢ LE.le (α := ℕ∞)
    (⨆ (_ :
      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})) :
          ℕ∞))
have a : ∀
  (i :
    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 ≤
      ⊤),
  LE.le (α := ℕ∞)
    (↑(p.length (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 : 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 iSup_le
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (↑(Set.Iic x) : Type u_1)
i :
  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 ≤
    ⊤
⊢ LE.le (α := ℕ∞)
    (↑(p.length (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 : 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})) :
          ℕ∞))
have mono : StrictMono (β := α) fun (y : (↑(Set.Iic x) : Type u_1)) ↦ (↑y : α)
Tactic: have mono : StrictMono (fun (y : Set.Iic x) ↦ y.1) := fun _ _ h ↦ h
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (↑(Set.Iic x) : Type u_1)
i :
  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 ≤
    ⊤
mono : StrictMono (β := α) fun (y : (↑(Set.Iic x) : Type u_1)) ↦ (↑y : α)
⊢ LE.le (α := ℕ∞)
    (↑(p.length (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 : 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})) :
          ℕ∞))
have a : LE.le (α := ℕ∞)
  (↑((p.map (fun (x_1 : (↑(Set.Iic x) : Type u_1)) ↦ (↑x_1 : α)) mono).length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x 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: rw [← LTSeries.map_length p (fun x ↦ x.1) mono, ]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (↑(Set.Iic x) : Type u_1)
i :
  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 ≤
    ⊤
mono : StrictMono (β := α) fun (y : (↑(Set.Iic x) : Type u_1)) ↦ (↑y : α)
⊢ LE.le (α := ℕ∞)
    (↑((p.map (fun (x_1 : (↑(Set.Iic x) : Type u_1)) ↦ (↑x_1 : α)) mono).length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x 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})) :
          ℕ∞))
have a : RelSeries.last (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (p.map (fun (x_1 : (↑(Set.Iic x) : Type u_1)) ↦ (↑x_1 : α)) mono) ≤
  x
Tactic: refine le_iSup₂ (f := fun p hp ↦ (p.length : ℕ∞)) (p.map (fun x ↦ x.1) mono) ?_
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_3
inst : Preorder α
x : α
⊢ (↑(coheight x) : WithBot ℕ∞) = krullDim.{u_3} (↑(Set.Ici x) : Type u_3)
have rw : (↑(height x) : WithBot ℕ∞) = krullDim.{u_3} (↑(Set.Ici x) : Type u_3)ᵒᵈ
Tactic: rw [coheight, ← krullDim_orderDual, Order.krullDim_eq_of_orderIso (OrderIso.refl _)]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤
have pos : ∀ (h : Nonempty α), FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤
Tactic: by_cases h : Nonempty α
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
pos : ∀ (h : Nonempty α), FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤
⊢ FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤
have neg : ∀ (h : ¬Nonempty α), FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤
Tactic: by_cases h : Nonempty α
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
h : ¬Nonempty α
⊢ FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤
have neg : FiniteDimensionalOrder α → krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
h : ¬Nonempty α
neg : FiniteDimensionalOrder α → krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤
⊢ FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤
have neg₁ : krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤ → FiniteDimensionalOrder α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
x : α
⊢ coheight x < ⊤
have rw : (↑(coheight x) : WithBot ℕ∞) < (↑⊤ : WithBot ℕ∞)
Tactic: rw [← WithBot.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : FiniteDimensionalOrder α
x : α
⊢ (↑(coheight x) : WithBot ℕ∞) < (↑⊤ : WithBot ℕ∞)
have apply : krullDim α < (↑⊤ : WithBot ℕ∞)
Tactic: apply lt_of_le_of_lt (coheight_le_krullDim x)
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
⊢ krullDim α = 1 ↔ IsSimpleOrder α
have rw : krullDim α ≤ 1 ∧ 1 ≤ krullDim α ↔ IsSimpleOrder α
Tactic: rw [le_antisymm_iff, krullDim_le_one_iff_of_boundedOrder, WithBot.one_le_iff_pos,
    Order.krullDim_pos_iff_of_orderBot, isSimpleOrder_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
rw : krullDim α ≤ 1 ∧ 1 ≤ krullDim α ↔ IsSimpleOrder α
⊢ krullDim α = 1 ↔ IsSimpleOrder α
have rw₁ : (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ 1 ≤ krullDim α ↔ IsSimpleOrder α
Tactic: rw [le_antisymm_iff, krullDim_le_one_iff_of_boundedOrder, WithBot.one_le_iff_pos,
    Order.krullDim_pos_iff_of_orderBot, isSimpleOrder_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
rw : krullDim α ≤ 1 ∧ 1 ≤ krullDim α ↔ IsSimpleOrder α
rw₁ : (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ 1 ≤ krullDim α ↔ IsSimpleOrder α
⊢ krullDim α = 1 ↔ IsSimpleOrder α
have rw₂ : (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ 0 < krullDim α ↔ IsSimpleOrder α
Tactic: rw [le_antisymm_iff, krullDim_le_one_iff_of_boundedOrder, WithBot.one_le_iff_pos,
    Order.krullDim_pos_iff_of_orderBot, isSimpleOrder_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
rw : krullDim α ≤ 1 ∧ 1 ≤ krullDim α ↔ IsSimpleOrder α
rw₁ : (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ 1 ≤ krullDim α ↔ IsSimpleOrder α
rw₂ : (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ 0 < krullDim α ↔ IsSimpleOrder α
⊢ krullDim α = 1 ↔ IsSimpleOrder α
have rw₃ : (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ Nontrivial α ↔ IsSimpleOrder α
Tactic: rw [le_antisymm_iff, krullDim_le_one_iff_of_boundedOrder, WithBot.one_le_iff_pos,
    Order.krullDim_pos_iff_of_orderBot, isSimpleOrder_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
rw : krullDim α ≤ 1 ∧ 1 ≤ krullDim α ↔ IsSimpleOrder α
rw₁ : (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ 1 ≤ krullDim α ↔ IsSimpleOrder α
rw₂ : (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ 0 < krullDim α ↔ IsSimpleOrder α
rw₃ : (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ Nontrivial α ↔ IsSimpleOrder α
⊢ krullDim α = 1 ↔ IsSimpleOrder α
have rw₄ : (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ Nontrivial α ↔ Nontrivial α ∧ ∀ (a : α), a = ⊥ ∨ a = ⊤
Tactic: rw [le_antisymm_iff, krullDim_le_one_iff_of_boundedOrder, WithBot.one_le_iff_pos,
    Order.krullDim_pos_iff_of_orderBot, isSimpleOrder_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
rw : krullDim α ≤ 1 ∧ 1 ≤ krullDim α ↔ IsSimpleOrder α
rw₁ : (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ 1 ≤ krullDim α ↔ IsSimpleOrder α
rw₂ : (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ 0 < krullDim α ↔ IsSimpleOrder α
rw₃ : (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ Nontrivial α ↔ IsSimpleOrder α
rw₄ : (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ Nontrivial α ↔ Nontrivial α ∧ ∀ (a : α), a = ⊥ ∨ a = ⊤
⊢ krullDim α = 1 ↔ IsSimpleOrder α
have rw₅ : (Nontrivial α ∧ ∀ (x : α), x = ⊥ ∨ x = ⊤) ↔ Nontrivial α ∧ ∀ (a : α), a = ⊥ ∨ a = ⊤
Tactic: rw [le_antisymm_iff, krullDim_le_one_iff_of_boundedOrder, WithBot.one_le_iff_pos,
    Order.krullDim_pos_iff_of_orderBot, isSimpleOrder_iff, and_comm]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
n : ℕ
ih : ∀ m < n, height m = (↑m : ℕ∞)
⊢ height n = (↑n : ℕ∞)
have ind : height n ≤ (↑n : ℕ∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
n : ℕ
ih : ∀ m < n, height m = (↑m : ℕ∞)
ind : height n ≤ (↑n : ℕ∞)
⊢ height n = (↑n : ℕ∞)
have ind₁ : (↑n : ℕ∞) ≤ height n
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
n : ℕ
ih : ∀ m < n, height m = (↑m : ℕ∞)
⊢ height n ≤ (↑n : ℕ∞)
have ind : ∀ y < n, height y < (↑n : ℕ∞)
Tactic: apply height_le_coe_iff.mpr
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
n : ℕ
⊢ height n = (↑n : ℕ∞)
have ind : ∀ (n : ℕ) (ih : ∀ m < n, height m = (↑m : ℕ∞)), height n = (↑n : ℕ∞)
Tactic: induction n using Nat.strongRecOn with | ind n ih =>
  apply le_antisymm
  · apply height_le_coe_iff.mpr
    simp +contextual only [ih, Nat.cast_lt, implies_true]
  · exact length_le_height_last (p := LTSeries.range n)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
⊢ coheight a = ⊤
have obtain : ∀ (f : ℕ → (↑(Set.Ioi a) : Type u_1)) (hstrictmono : StrictMono f), coheight a = ⊤
Tactic: obtain ⟨f, hstrictmono⟩ := Nat.exists_strictMono ↑(Set.Ioi a)
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
⊢ coheight a = ⊤
have apply : ∀ (n : ℕ),
  ∃ (p : LTSeries α),
    RelSeries.head (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a ∧
      p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        n
Tactic: apply coheight_eq_top_iff.mpr
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m : ℕ
⊢ ∃ (p : LTSeries α),
    RelSeries.head (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a ∧
      p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        m
have use : RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (RelSeries.mk (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        m (fun (i : Fin (m + 1)) ↦ if i = 0 then a else (↑(f (↑i : ℕ)) : α)) sorry) =
    a ∧
  RelSeries.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (RelSeries.mk (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        m (fun (i : Fin (m + 1)) ↦ if i = 0 then a else (↑(f (↑i : ℕ)) : α)) sorry) =
    m
Tactic: use { length := m, toFun := fun i => if i = 0 then a else f i, step := ?step }
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m : ℕ
use :
  RelSeries.head (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (RelSeries.mk (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          m (fun (i : Fin (m + 1)) ↦ if i = 0 then a else (↑(f (↑i : ℕ)) : α)) ⋯) =
      a ∧
    RelSeries.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        (RelSeries.mk (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          m (fun (i : Fin (m + 1)) ↦ if i = 0 then a else (↑(f (↑i : ℕ)) : α)) ⋯) =
      m
⊢ ∃ (p : LTSeries α),
    RelSeries.head (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a ∧
      p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) =
        m
have use₁ : ∀ (i : Fin m),
  Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (if i.castSucc = 0 then a else (↑(f (↑i.castSucc : ℕ)) : α), if i.succ = 0 then a else (↑(f (↑i.succ : ℕ)) : α))
Tactic: use { length := m, toFun := fun i => if i = 0 then a else f i, step := ?step }
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (if (⟨i, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).castSucc : ℕ)) : α),
      if (⟨i, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).succ : ℕ)) : α))
have pos : ∀ (hzero : i = 0),
  Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (if (⟨i, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).castSucc : ℕ)) : α),
      if (⟨i, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).succ : ℕ)) : α))
Tactic: by_cases hzero : i = 0
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
pos :
  ∀ (hzero : i = 0),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (if (⟨i, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).castSucc : ℕ)) : α),
        if (⟨i, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).succ : ℕ)) : α))
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (if (⟨i, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).castSucc : ℕ)) : α),
      if (⟨i, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).succ : ℕ)) : α))
have neg : ∀ (hzero : ¬i = 0),
  Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (if (⟨i, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).castSucc : ℕ)) : α),
      if (⟨i, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).succ : ℕ)) : α))
Tactic: by_cases hzero : i = 0
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : i = 0
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (if (⟨i, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).castSucc : ℕ)) : α),
      if (⟨i, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).succ : ℕ)) : α))
have pos : ∀ (hi : 0 < m),
  Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (if (⟨0, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨0, hi⟩ : Fin m).castSucc : ℕ)) : α),
      if (⟨0, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨0, hi⟩ : Fin m).succ : ℕ)) : α))
Tactic: subst i
Cleared hypotheses: i, hi, hzero
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
⊢ Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (if (⟨i, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).castSucc : ℕ)) : α),
      if (⟨i, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).succ : ℕ)) : α))
have neg : f i < f (i + 1)
Tactic: suffices f i < f (i + 1) by simp [Fin.ext_iff, hzero, this]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m i : ℕ
hi : i < m
hzero : ¬i = 0
⊢ f i < f (i + 1)
have neg : i < i + 1
Tactic: apply hstrictmono
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
f : ℕ → (↑(Set.Ioi a) : Type u_1)
hstrictmono : StrictMono f
m : ℕ
case case₁ :
  ∀ (h : Fin m),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (if h.castSucc = 0 then a else (↑(f (↑h.castSucc : ℕ)) : α), if h.succ = 0 then a else (↑(f (↑h.succ : ℕ)) : α))
⊢ ∀ (i : Fin m),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (if i.castSucc = 0 then a else (↑(f (↑i.castSucc : ℕ)) : α), if i.succ = 0 then a else (↑(f (↑i.succ : ℕ)) : α))
have case₂ : ∀ (h : Fin m) (i : ℕ) (hi : i < m),
  Membership.mem (γ := SetRel α α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b}
    (if (⟨i, hi⟩ : Fin m).castSucc = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).castSucc : ℕ)) : α),
      if (⟨i, hi⟩ : Fin m).succ = 0 then a else (↑(f (↑(⟨i, hi⟩ : Fin m).succ : ℕ)) : α))
Tactic: case step =>
    intro ⟨i, hi⟩
    by_cases hzero : i = 0
    · subst i
      exact (f 1).prop
    · suffices f i < f (i + 1) by simp [Fin.ext_iff, hzero, this]
      apply hstrictmono
      lia