awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ ⨆ (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 α)
have a : ∀ (i : LTSeries α)
  (j :
    RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        i =
      x),
  HAdd.hAdd (α := ℕ∞)
      (↑(i.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
      1 ≤
    height (↑x : WithBot α)
Tactic: apply iSup₂_le
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ height (↑x : WithTop α) = height x
have a : height (↑x : WithTop α) ≤ height x
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
a : height (↑x : WithTop α) ≤ height x
⊢ height (↑x : WithTop α) = height x
have a₁ : height x ≤ height (↑x : WithTop α)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ height (↑x : WithTop α) ≤ height x
have a : ∀ (p : LTSeries (WithTop α)),
  RelSeries.last (r :=
        {x : WithTop α × WithTop α |
          match (motive := WithTop α × WithTop α → Prop) x with
          | (a, b) => a < b})
        p =
      (↑x : WithTop α) →
    (↑(p.length (r :=
            {x : WithTop α × WithTop α |
              match (motive := WithTop α × WithTop α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) ≤
      height x
Tactic: apply height_le
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (WithTop α)
hlast :
  RelSeries.last (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithTop α)
i :
  Fin
    (p.length (r :=
        {x : WithTop α × WithTop α |
          match (motive := WithTop α × WithTop α → Prop) x with
          | (a, b) => a < b}) +
      1)
⊢ p.toFun (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      i ≠
    ⊤
have apply : p.toFun (r :=
    {x : WithTop α × WithTop α |
      match (motive := WithTop α × WithTop α → Prop) x with
      | (a, b) => a < b})
    i <
  ⊤
Tactic: apply WithTop.lt_top_iff_ne_top.mp
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (WithTop α)
hlast :
  RelSeries.last (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithTop α)
i :
  Fin
    (p.length (r :=
        {x : WithTop α × WithTop α |
          match (motive := WithTop α × WithTop α → Prop) x with
          | (a, b) => a < b}) +
      1)
⊢ p.toFun (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      i <
    ⊤
have hab : p.toFun (r :=
    {x : WithTop α × WithTop α |
      match (motive := WithTop α × WithTop α → Prop) x with
      | (a, b) => a < b})
    i ≤
  p.toFun (r :=
    {x : WithTop α × WithTop α |
      match (motive := WithTop α × WithTop α → Prop) x with
      | (a, b) => a < b})
    (Fin.last
      (p.length (r :=
        {x : WithTop α × WithTop α |
          match (motive := WithTop α × WithTop α → Prop) x with
          | (a, b) => a < b})))
Tactic: apply lt_of_le_of_lt
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (WithTop α)
hlast :
  RelSeries.last (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithTop α)
i :
  Fin
    (p.length (r :=
        {x : WithTop α × WithTop α |
          match (motive := WithTop α × WithTop α → Prop) x with
          | (a, b) => a < b}) +
      1)
hab :
  p.toFun (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      i ≤
    p.toFun (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      (Fin.last
        (p.length (r :=
          {x : WithTop α × WithTop α |
            match (motive := WithTop α × WithTop α → Prop) x with
            | (a, b) => a < b})))
⊢ p.toFun (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      i <
    ⊤
have hbc : p.toFun (r :=
    {x : WithTop α × WithTop α |
      match (motive := WithTop α × WithTop α → Prop) x with
      | (a, b) => a < b})
    (Fin.last
      (p.length (r :=
        {x : WithTop α × WithTop α |
          match (motive := WithTop α × WithTop α → Prop) x with
          | (a, b) => a < b}))) <
  ⊤
Tactic: apply lt_of_le_of_lt
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (WithTop α)
hlast :
  RelSeries.last (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithTop α)
i :
  Fin
    (p.length (r :=
        {x : WithTop α × WithTop α |
          match (motive := WithTop α × WithTop α → Prop) x with
          | (a, b) => a < b}) +
      1)
hab :
  p.toFun (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      i ≤
    p.toFun (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      (Fin.last
        (p.length (r :=
          {x : WithTop α × WithTop α |
            match (motive := WithTop α × WithTop α → Prop) x with
            | (a, b) => a < b})))
hbc :
  p.toFun (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      (Fin.last
        (p.length (r :=
          {x : WithTop α × WithTop α |
            match (motive := WithTop α × WithTop α → Prop) x with
            | (a, b) => a < b}))) <
    ⊤
⊢ p.toFun (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      i <
    ⊤
have b : WithTop α
Tactic: apply lt_of_le_of_lt
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (WithTop α)
hlast :
  RelSeries.last (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithTop α)
i :
  Fin
    (p.length (r :=
        {x : WithTop α × WithTop α |
          match (motive := WithTop α × WithTop α → Prop) x with
          | (a, b) => a < b}) +
      1)
⊢ p.toFun (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      (Fin.last
        (p.length (r :=
          {x : WithTop α × WithTop α |
            match (motive := WithTop α × WithTop α → Prop) x with
            | (a, b) => a < b}))) <
    ⊤
have hbc : ∀
  (hlast :
    p.toFun (r :=
        {x : WithTop α × WithTop α |
          match (motive := WithTop α × WithTop α → Prop) x with
          | (a, b) => a < b})
        (Fin.last
          (p.length (r :=
            {x : WithTop α × WithTop α |
              match (motive := WithTop α × WithTop α → Prop) x with
              | (a, b) => a < b}))) =
      (↑x : WithTop α))
  (i :
    Fin
      (p.length (r :=
          {x : WithTop α × WithTop α |
            match (motive := WithTop α × WithTop α → Prop) x with
            | (a, b) => a < b}) +
        1)),
  p.toFun (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      (Fin.last
        (p.length (r :=
          {x : WithTop α × WithTop α |
            match (motive := WithTop α × WithTop α → Prop) x with
            | (a, b) => a < b}))) <
    ⊤
Tactic: rw [RelSeries.last] at hlast
Cleared hypotheses: hlast, i
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (WithTop α)
hlast :
  RelSeries.last (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithTop α)
p' : LTSeries α :=
  RelSeries.mk (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (p.length (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b}))
    (fun
        (i :
          Fin
            (p.length (r :=
                {x : WithTop α × WithTop α |
                  match (motive := WithTop α × WithTop α → Prop) x with
                  | (a, b) => a < b}) +
              1)) ↦
      (p.toFun (r :=
            {x : WithTop α × WithTop α |
              match (motive := WithTop α × WithTop α → Prop) x with
              | (a, b) => a < b})
            i).untop
        ⋯)
    ⋯
⊢ (↑(p.length (r :=
          {x : WithTop α × WithTop α |
            match (motive := WithTop α × WithTop α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x
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, WithTop.untop_eq_iff, ← hlast]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (WithTop α)
hlast :
  RelSeries.last (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithTop α)
p' : LTSeries α :=
  RelSeries.mk (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (p.length (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b}))
    (fun
        (i :
          Fin
            (p.length (r :=
                {x : WithTop α × WithTop α |
                  match (motive := WithTop α × WithTop α → Prop) x with
                  | (a, b) => a < b}) +
              1)) ↦
      (p.toFun (r :=
            {x : WithTop α × WithTop α |
              match (motive := WithTop α × WithTop α → Prop) x with
              | (a, b) => a < b})
            i).untop
        ⋯)
    ⋯
hlast' :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p' =
    x
this :
  (↑(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')
⊢ (↑(p.length (r :=
          {x : WithTop α × WithTop α |
            match (motive := WithTop α × WithTop α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x
have this₁ : (↑(p'.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})) :
    ℕ∞) ≤
  height x
Tactic: rw [hlast'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
p : LTSeries (WithTop α)
hlast :
  RelSeries.last (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b})
      p =
    (↑x : WithTop α)
p' : LTSeries α :=
  RelSeries.mk (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    (p.length (r :=
      {x : WithTop α × WithTop α |
        match (motive := WithTop α × WithTop α → Prop) x with
        | (a, b) => a < b}))
    (fun
        (i :
          Fin
            (p.length (r :=
                {x : WithTop α × WithTop α |
                  match (motive := WithTop α × WithTop α → Prop) x with
                  | (a, b) => a < b}) +
              1)) ↦
      (p.toFun (r :=
            {x : WithTop α × WithTop α |
              match (motive := WithTop α × WithTop α → Prop) x with
              | (a, b) => a < b})
            i).untop
        ⋯)
    ⋯
hlast' :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p' =
    x
⊢ (↑(p.length (r :=
          {x : WithTop α × WithTop α |
            match (motive := WithTop α × WithTop α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    height x
have a : (↑(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
      rw [hlast'] at this
      simpa [p'] using this
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ height x ≤ height (↑x : WithTop α)
have a : ∀ (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})) :
        ℕ∞) ≤
      height (↑x : WithTop α)
Tactic: apply height_le
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ krullDim.{u_1} (WithTop α) = krullDim α + 1
have rw : (↑(⨆ (y : WithTop α), ⨆ (_ : y < ⊤), height y + 1) : WithBot ℕ∞) =
  HAdd.hAdd (α := WithBot ℕ∞) (↑(⨆ (a : α), height a) : WithBot ℕ∞) 1
Tactic: rw [← height_top_eq_krullDim, krullDim_eq_iSup_height_of_nonempty, height_eq_iSup_lt_height]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ (↑(⨆ (y : WithTop α), ⨆ (_ : y < ⊤), height y + 1) : WithBot ℕ∞) =
    HAdd.hAdd (α := WithBot ℕ∞) (↑(⨆ (a : α), height a) : WithBot ℕ∞) 1
have norm_cast : ⨆ (y : WithTop α), ⨆ (_ : y < ⊤), height y + 1 = HAdd.hAdd (α := ℕ∞) (⨆ (a : α), height a) 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ ⨆ (y : WithTop α), ⨆ (_ : y < ⊤), height y + 1 = HAdd.hAdd (α := ℕ∞) (⨆ (a : α), height a) 1
have simp_rw : ⨆ (y : WithTop α), ⨆ (_ : y ≠ ⊤), height y + 1 = HAdd.hAdd (α := ℕ∞) (⨆ (a : α), height a) 1
Tactic: simp_rw [WithTop.lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ ⨆ (y : WithTop α), ⨆ (_ : y ≠ ⊤), height y + 1 = HAdd.hAdd (α := ℕ∞) (⨆ (a : α), height a) 1
have rw : Eq (α := ℕ∞) (⨆ (x : { y : WithTop α // y ≠ ⊤ }), height (↑x : WithTop α) + 1) (⨆ (i : α), height i + 1)
Tactic: rw [ENat.iSup_add, iSup_subtype']
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ Eq (α := ℕ∞) (⨆ (x : { y : WithTop α // y ≠ ⊤ }), height (↑x : WithTop α) + 1) (⨆ (i : α), height i + 1)
have symm : Eq (α := ℕ∞) (⨆ (i : α), height i + 1) (⨆ (x : { y : WithTop α // y ≠ ⊤ }), height (↑x : WithTop α) + 1)
Tactic: symm
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ Eq (α := ℕ∞) (⨆ (i : α), height i + 1) (⨆ (x : { y : WithTop α // y ≠ ⊤ }), height (↑x : WithTop α) + 1)
have apply : ∀ (x : α),
  height.{u_1} (α := WithTop α)
        (↑((Equiv.symm Equiv.withTopSubtypeNe : (a : α) → { y : WithTop α // y ≠ ⊤ }) x) : WithTop α) +
      1 =
    height x + 1
Tactic: apply Equiv.withTopSubtypeNe.symm.iSup_congr
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
| krullDim.{u_1} (WithBot α)
have rw : krullDim.{u_1} (WithBot α)ᵒᵈ
Tactic: rw [← krullDim_orderDual]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ krullDim.{u_1} (WithBot α) = krullDim α + 1
have conv_lhs : krullDim.{u_1} (WithBot α)ᵒᵈ = krullDim α + 1
Tactic: conv_lhs => rw [← krullDim_orderDual]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
| krullDim α + 1
have rw : krullDim.{u_1} αᵒᵈ + 1
Tactic: rw [← krullDim_orderDual]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ krullDim.{u_1} (WithBot α)ᵒᵈ = krullDim α + 1
have conv_rhs : krullDim.{u_1} (WithBot α)ᵒᵈ = krullDim.{u_1} αᵒᵈ + 1
Tactic: conv_rhs => rw [← krullDim_orderDual]
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
n : ℕ∞
⊢ height n = n
have top : height (α := ℕ∞) ⊤ = ⊤
Tactic: cases n with
  | top => simp only [← WithBot.coe_eq_coe, height_top_eq_krullDim, krullDim_enat, WithBot.coe_top]
  | coe n => exact (height_coe_withTop _).trans (height_nat _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
n : ℕ∞
top : height (α := ℕ∞) ⊤ = ⊤
⊢ height n = n
have coe : ∀ (n : ℕ), height (α := ℕ∞) (↑n : ℕ∞) = (↑n : ℕ∞)
Tactic: cases n with
  | top => simp only [← WithBot.coe_eq_coe, height_top_eq_krullDim, krullDim_enat, WithBot.coe_top]
  | coe n => exact (height_coe_withTop _).trans (height_nat _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
n : ℕ
⊢ coheight (α := ℕ∞) (↑n : ℕ∞) = ⊤
have apply : coheight n + 1 = ⊤
Tactic: apply (coheight_coe_withTop _).trans
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
x : α
⊢ height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * height.{u_2} (α := β) ((f : (a : α) → β) x : β) + (↑m : ℕ∞)
have generalize : ∀ (n : ℕ∞) (h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = n),
  height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * n + (↑m : ℕ∞)
Tactic: generalize h' : Order.height (f x) = n
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ (x : α) (h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑m_1 : ℕ∞)),
      height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑m_1 : ℕ∞) + (↑m : ℕ∞)
x : α
h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑n : ℕ∞)
⊢ height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n : ℕ∞) + (↑m : ℕ∞)
have coe : ∀ (p : LTSeries α)
  (hp :
    RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p ≤
      x)
  (h_len :
    HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n : ℕ∞) + (↑m : ℕ∞) <
      (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)),
  False
Tactic: refine height_le_iff.mpr fun p hp ↦ le_of_not_gt fun h_len ↦ ?_
-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ (x : α) (h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑m_1 : ℕ∞)),
      height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑m_1 : ℕ∞) + (↑m : ℕ∞)
x : α
h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑n : ℕ∞)
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
h_len :
  HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n : ℕ∞) + (↑m : ℕ∞) <
    (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
i : Fin
  (p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) +
    1) :=
  ⟨p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) -
      (m + 1),
    ⋯⟩
h'' :
  LT.lt.{u_2} (α := β)
    ((f : (a : α) → β)
        (p.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i) :
      β)
    ((f : (a : α) → β) x : β)
⊢ False
have obtain : ∀ (n' : ℕ)
  (hn' :
    (↑n' : ℕ∞) =
      height.{u_2} (α := β)
        ((f : (a : α) → β)
            (p.toFun (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              i) :
          β)),
  False
Tactic: obtain ⟨n', hn'⟩ : ∃ (n' : ℕ), n' = height (f (p i)) := ENat.ne_top_iff_exists.mp
        ((height_mono h''.le).trans_lt (h' ▸ ENat.coe_lt_top _)).ne
-- Lean 4 proof step from Mathlib.Order.KrullDimension (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim.{u_1} (↑(Set.preimage (β := β) (⇑f : (a : α) → β) {x}) : Type u_1) ≤ (↑m : WithBot ℕ∞)
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ (x : α) (h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑m_1 : ℕ∞)),
      height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑m_1 : ℕ∞) + (↑m : ℕ∞)
x : α
h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑n : ℕ∞)
p : LTSeries α
hp :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    x
h_len :
  HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n : ℕ∞) + (↑m : ℕ∞) <
    (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
i : Fin
  (p.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) +
    1) :=
  ⟨p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) -
      (m + 1),
    ⋯⟩
h'' :
  LT.lt.{u_2} (α := β)
    ((f : (a : α) → β)
        (p.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i) :
      β)
    ((f : (a : α) → β) x : β)
n' : ℕ
hn' :
  (↑n' : ℕ∞) =
    height.{u_2} (α := β)
      ((f : (a : α) → β)
          (p.toFun (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            i) :
        β)
⊢ False
have h_lt : n' < n
Tactic: have h_lt : n' < n := ENat.coe_lt_coe.mp
        (h' ▸ hn' ▸ height_strictMono h'' (hn' ▸ ENat.coe_lt_top _))