awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ)) : α))
case₂ 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 : ℕ)) : α))
⊢ ∀ (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₄ : ∀ (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
-- 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 : ℕ)) : α))
case₂ 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 : ℕ)) : α))
case₄ :
  ∀ (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 : ℕ)) : α))
⊢ ∀ (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 pos : ∀ (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 : ℕ)) : α))
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
-- 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 : ℕ)) : α))
case₂ 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 : ℕ)) : α))
case₄ :
  ∀ (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 : ℕ)) : α))
pos :
  ∀ (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 : ℕ)) : α))
⊢ ∀ (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 neg : ∀ (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 : ℕ)) : α))
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
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ height (↑x : WithBot α) = height x + 1
have a : height (↑x : WithBot α) ≤ height x + 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
a : height (↑x : WithBot α) ≤ height x + 1
⊢ height (↑x : WithBot α) = height x + 1
have a₁ : height x + 1 ≤ height (↑x : WithBot α)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ height (↑x : WithBot α) ≤ height x + 1
have a : ∀ (p : LTSeries (WithBot α)),
  RelSeries.last (r :=
        {x : WithBot α × WithBot α |
          match (motive := WithBot α × WithBot α → Prop) x with
          | (a, b) => a < b})
        p =
      (↑x : WithBot α) →
    (↑(p.length (r :=
            {x : WithBot α × WithBot α |
              match (motive := WithBot α × WithBot α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) ≤
      height x + 1
Tactic: apply height_le
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (WithBot α)
hlast :
  RelSeries.last (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithBot α)
⊢ (↑(p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x + 1
have a : ∀
  (this :
    ∀ {α : Type u_1} [inst : Preorder α] (x : α) (p : LTSeries (WithBot α))
      (hlast :
        RelSeries.last (r :=
            {x : WithBot α × WithBot α |
              match (motive := WithBot α × WithBot α → Prop) x with
              | (a, b) => a < b})
            p =
          (↑x : WithBot α))
      (hlenpos :
        p.length (r :=
            {x : WithBot α × WithBot α |
              match (motive := WithBot α × WithBot α → Prop) x with
              | (a, b) => a < b}) ≠
          0),
      (↑(p.length (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        height x + 1)
  (hlenpos :
    ¬p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b}) ≠
        0),
  (↑(p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x + 1
Tactic: wlog hlenpos : p.length ≠ 0
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (WithBot α)
hlast :
  RelSeries.last (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithBot α)
a :
  ∀
    (this :
      ∀ {α : Type u_1} [inst : Preorder α] (x : α) (p : LTSeries (WithBot α))
        (hlast :
          RelSeries.last (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b})
              p =
            (↑x : WithBot α))
        (hlenpos :
          p.length (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b}) ≠
            0),
        (↑(p.length (r :=
                {x : WithBot α × WithBot α |
                  match (motive := WithBot α × WithBot α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) ≤
          height x + 1)
    (hlenpos :
      ¬p.length (r :=
            {x : WithBot α × WithBot α |
              match (motive := WithBot α × WithBot α → Prop) x with
              | (a, b) => a < b}) ≠
          0),
    (↑(p.length (r :=
            {x : WithBot α × WithBot α |
              match (motive := WithBot α × WithBot α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) ≤
      height x + 1
⊢ (↑(p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x + 1
have wlog : ∀ {α : Type u_1} [inst : Preorder α] (x : α) (p : LTSeries (WithBot α))
  (hlast :
    RelSeries.last (r :=
        {x : WithBot α × WithBot α |
          match (motive := WithBot α × WithBot α → Prop) x with
          | (a, b) => a < b})
        p =
      (↑x : WithBot α))
  (hlenpos :
    p.length (r :=
        {x : WithBot α × WithBot α |
          match (motive := WithBot α × WithBot α → Prop) x with
          | (a, b) => a < b}) ≠
      0),
  (↑(p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x + 1
Tactic: wlog hlenpos : p.length ≠ 0
Cleared hypotheses: x, p, hlast
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
p : LTSeries (WithBot α)
hlast :
  RelSeries.last (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithBot α)
hlenpos :
  p.length (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b}) ≠
    0
x_1 :
  Fin
    (p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b}) -
        1 +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b}) -
        1 +
      1
⊢ p.toFun (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      (⟨i + 1, ⋯⟩ :
        Fin
          (p.length (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b}) +
            1)) ≠
    ⊥
have apply : RelSeries.head (r :=
    {x : WithBot α × WithBot α |
      match (motive := WithBot α × WithBot α → Prop) x with
      | (a, b) => a < b})
    p <
  p.toFun (r :=
    {x : WithBot α × WithBot α |
      match (motive := WithBot α × WithBot α → Prop) x with
      | (a, b) => a < b})
    ⟨i + 1, sorry⟩
Tactic: apply ne_bot_of_gt (b := p.head)
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
p : LTSeries (WithBot α)
hlast :
  RelSeries.last (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithBot α)
hlenpos :
  p.length (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b}) ≠
    0
x_1 :
  Fin
    (p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b}) -
        1 +
      1)
i : ℕ
hi :
  i <
    p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b}) -
        1 +
      1
⊢ RelSeries.head (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p <
    p.toFun (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      ⟨i + 1, ⋯⟩
have a : 0 <
  (⟨i + 1, sorry⟩ :
    Fin
      (p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b}) +
        1))
Tactic: apply p.strictMono
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
p : LTSeries (WithBot α)
hlast :
  RelSeries.last (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithBot α)
hlenpos :
  p.length (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : LTSeries α :=
  RelSeries.mk (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (p.length (r :=
        {x : WithBot α × WithBot α |
          match (motive := WithBot α × WithBot α → Prop) x with
          | (a, b) => a < b}) -
      1)
    (fun
        (x :
          Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1)) ↦
      match (motive :=
        Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1) →
          α)
        x with
      | ⟨i, hi⟩ =>
        (p.toFun (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b})
              ⟨i + 1, ⋯⟩).unbot
          ⋯)
    ⋯
⊢ RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p' =
    x
have simp : p.toFun (r := {x : WithBot α × WithBot α | x.1 < x.2})
    (⟨p.length (r := {x : WithBot α × WithBot α | x.1 < x.2}) - 1 + 1, sorry⟩ :
      Fin (p.length (r := {x : WithBot α × WithBot α | x.1 < x.2}) + 1)) =
  p.toFun (r := {x : WithBot α × WithBot α | x.1 < x.2}) ⟨p.length (r := {x : WithBot α × WithBot α | x.1 < x.2}), sorry⟩
Tactic: simp only [p', RelSeries.last, WithBot.unbot_eq_iff, ← hlast, Fin.last]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
p : LTSeries (WithBot α)
hlast :
  RelSeries.last (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithBot α)
hlenpos :
  p.length (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : LTSeries α :=
  RelSeries.mk (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (p.length (r :=
        {x : WithBot α × WithBot α |
          match (motive := WithBot α × WithBot α → Prop) x with
          | (a, b) => a < b}) -
      1)
    (fun
        (x :
          Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1)) ↦
      match (motive :=
        Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1) →
          α)
        x with
      | ⟨i, hi⟩ =>
        (p.toFun (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b})
              ⟨i + 1, ⋯⟩).unbot
          ⋯)
    ⋯
⊢ p.toFun (r := {x : WithBot α × WithBot α | x.1 < x.2})
      (⟨p.length (r := {x : WithBot α × WithBot α | x.1 < x.2}) - 1 + 1, ⋯⟩ :
        Fin (p.length (r := {x : WithBot α × WithBot α | x.1 < x.2}) + 1)) =
    p.toFun (r := {x : WithBot α × WithBot α | x.1 < x.2}) ⟨p.length (r := {x : WithBot α × WithBot α | x.1 < x.2}), ⋯⟩
have e_a : p.length (r := {x : WithBot α × WithBot α | x.1 < x.2}) - 1 + 1 =
  p.length (r := {x : WithBot α × WithBot α | x.1 < x.2})
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
p : LTSeries (WithBot α)
hlast :
  RelSeries.last (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithBot α)
hlenpos :
  p.length (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : LTSeries α :=
  RelSeries.mk (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (p.length (r :=
        {x : WithBot α × WithBot α |
          match (motive := WithBot α × WithBot α → Prop) x with
          | (a, b) => a < b}) -
      1)
    (fun
        (x :
          Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1)) ↦
      match (motive :=
        Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1) →
          α)
        x with
      | ⟨i, hi⟩ =>
        (p.toFun (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b})
              ⟨i + 1, ⋯⟩).unbot
          ⋯)
    ⋯
⊢ (↑(p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x + 1
have hlast' : RelSeries.last (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    p' =
  x
Tactic: have hlast' : p'.last = x := by
      simp only [p', RelSeries.last, WithBot.unbot_eq_iff, ← hlast, Fin.last]
      congr
      lia
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
x : α
p : LTSeries (WithBot α)
hlast :
  RelSeries.last (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithBot α)
hlenpos :
  p.length (r :=
      {x : WithBot α × WithBot α |
        match (motive := WithBot α × WithBot α → Prop) x with
        | (a, b) => a < b}) ≠
    0
p' : LTSeries α :=
  RelSeries.mk (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (p.length (r :=
        {x : WithBot α × WithBot α |
          match (motive := WithBot α × WithBot α → Prop) x with
          | (a, b) => a < b}) -
      1)
    (fun
        (x :
          Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1)) ↦
      match (motive :=
        Fin
            (p.length (r :=
                  {x : WithBot α × WithBot α |
                    match (motive := WithBot α × WithBot α → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1) →
          α)
        x with
      | ⟨i, hi⟩ =>
        (p.toFun (r :=
              {x : WithBot α × WithBot α |
                match (motive := WithBot α × WithBot α → Prop) x with
                | (a, b) => a < b})
              ⟨i + 1, ⋯⟩).unbot
          ⋯)
    ⋯
hlast' :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p' =
    x
⊢ (↑(p.length (r :=
          {x : WithBot α × WithBot α |
            match (motive := WithBot α × WithBot α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x + 1
have suffices : (↑(p'.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})) :
    ℕ∞) ≤
  height
    (RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p')
Tactic: suffices p'.length ≤ height p'.last by
      simpa [p', hlast'] using this
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ height x + 1 ≤ height (↑x : WithBot α)
have a : ⨆ (p : LTSeries α),
    ⨆ (_ :
      RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        x),
      HAdd.hAdd (α := ℕ∞)
        (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)
        1 ≤
  height (↑x : WithBot α)
Tactic: rw [height_add_const]