awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) :
        β)
h_lt : n' < n
⊢ False
have this : (↑((RelSeries.take (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p i).length
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})) :
    ℕ∞) ≤
  HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n' : ℕ∞) + (↑m : ℕ∞)
Tactic: have := (length_le_height_last (p := p.take i)).trans <| ih n' h_lt (p i) hn'.symm
-- 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) :
        β)
h_lt : n' < n
this :
  (↑((RelSeries.take (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p i).length
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n' : ℕ∞) + (↑m : ℕ∞)
⊢ False
have this₁ : (↑(p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})) :
    ℕ∞) ≤
  HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * HAdd.hAdd (α := ℕ∞) (↑n' : ℕ∞) 1 + (↑m : ℕ∞)
Tactic: rw [RelSeries.take_length, ENat.coe_sub, Nat.cast_add, Nat.cast_one, tsub_le_iff_right,
        add_assoc, add_comm _ (_ + 1), ← add_assoc, ← mul_add_one] at this
Cleared hypotheses: this
-- 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 : β)
n' : ℕ
hn' :
  (↑n' : ℕ∞) =
    height.{u_2} (α := β)
      ((f : (a : α) → β)
          (p.toFun (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            i) :
        β)
h_lt : n' < n
this :
  (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * HAdd.hAdd (α := ℕ∞) (↑n' : ℕ∞) 1 + (↑m : ℕ∞)
⊢ False
have refine : HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * HAdd.hAdd (α := ℕ∞) (↑n' : ℕ∞) 1 + (↑m : ℕ∞) ≤
  HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n : ℕ∞) + (↑m : ℕ∞)
Tactic: refine not_lt_of_ge ?_ (h_len.trans_le this)
-- 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 : β)
n' : ℕ
hn' :
  (↑n' : ℕ∞) =
    height.{u_2} (α := β)
      ((f : (a : α) → β)
          (p.toFun (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            i) :
        β)
h_lt : n' < n
this :
  (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * HAdd.hAdd (α := ℕ∞) (↑n' : ℕ∞) 1 + (↑m : ℕ∞)
⊢ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * HAdd.hAdd (α := ℕ∞) (↑n' : ℕ∞) 1 + (↑m : ℕ∞) ≤
    HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n : ℕ∞) + (↑m : ℕ∞)
have bc : HAdd.hAdd (α := ℕ∞) (↑n' : ℕ∞) 1 ≤ (↑n : ℕ∞)
Tactic: gcongr
-- 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 : β)
n' : ℕ
hn' :
  (↑n' : ℕ∞) =
    height.{u_2} (α := β)
      ((f : (a : α) → β)
          (p.toFun (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            i) :
        β)
h_lt : n' < n
this :
  (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * HAdd.hAdd (α := ℕ∞) (↑n' : ℕ∞) 1 + (↑m : ℕ∞)
⊢ HAdd.hAdd (α := ℕ∞) (↑n' : ℕ∞) 1 ≤ (↑n : ℕ∞)
have bc : HAdd.hAdd (α := ℕ∞) (↑n' : ℕ∞) (↑1 : ℕ∞) ≤ (↑n : ℕ∞)
Tactic: rwa [← ENat.coe_one, ← ENat.coe_add, ENat.coe_le_coe]
-- 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 : β)
n' : ℕ
hn' :
  (↑n' : ℕ∞) =
    height.{u_2} (α := β)
      ((f : (a : α) → β)
          (p.toFun (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            i) :
        β)
h_lt : n' < n
this :
  (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * HAdd.hAdd (α := ℕ∞) (↑n' : ℕ∞) 1 + (↑m : ℕ∞)
bc : HAdd.hAdd (α := ℕ∞) (↑n' : ℕ∞) (↑1 : ℕ∞) ≤ (↑n : ℕ∞)
⊢ HAdd.hAdd (α := ℕ∞) (↑n' : ℕ∞) 1 ≤ (↑n : ℕ∞)
have bc₁ : LE.le (α := ℕ∞) (↑(n' + 1) : ℕ∞) (↑n : ℕ∞)
Tactic: rwa [← ENat.coe_one, ← ENat.coe_add, ENat.coe_le_coe]
-- 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 : β)
n' : ℕ
hn' :
  (↑n' : ℕ∞) =
    height.{u_2} (α := β)
      ((f : (a : α) → β)
          (p.toFun (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            i) :
        β)
h_lt : n' < n
this :
  (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * HAdd.hAdd (α := ℕ∞) (↑n' : ℕ∞) 1 + (↑m : ℕ∞)
bc : HAdd.hAdd (α := ℕ∞) (↑n' : ℕ∞) (↑1 : ℕ∞) ≤ (↑n : ℕ∞)
bc₁ : LE.le (α := ℕ∞) (↑(n' + 1) : ℕ∞) (↑n : ℕ∞)
⊢ HAdd.hAdd (α := ℕ∞) (↑n' : ℕ∞) 1 ≤ (↑n : ℕ∞)
have bc₂ : n' + 1 ≤ n
Tactic: rwa [← ENat.coe_one, ← ENat.coe_add, ENat.coe_le_coe]
-- 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),
    ⋯⟩
⊢ False
have coe : LT.lt.{u_2} (α := β)
  ((f : (a : α) → β)
      (p.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        i) :
    β)
  ((f : (a : α) → β) x : β)
Tactic: suffices h'' : f (p i) < f x by
      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
      have h_lt : n' < n := ENat.coe_lt_coe.mp
        (h' ▸ hn' ▸ height_strictMono h'' (hn' ▸ ENat.coe_lt_top _))
      have := (length_le_height_last (p := p.take i)).trans <| ih n' h_lt (p i) hn'.symm
      rw [RelSeries.take_length, ENat.coe_sub, Nat.cast_add, Nat.cast_one, tsub_le_iff_right,
        add_assoc, add_comm _ (_ + 1), ← add_assoc, ← mul_add_one] at this
      refine not_lt_of_ge ?_ (h_len.trans_le this)
      gcongr
      rwa [← ENat.coe_one, ← ENat.coe_add, ENat.coe_le_coe]
-- 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),
    ⋯⟩
⊢ LT.lt.{u_2} (α := β)
    ((f : (a : α) → β)
        (p.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i) :
      β)
    ((f : (a : α) → β) x : β)
have coe : ∀
  (h'' :
    LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β)
      ((f : (a : α) → β)
          (p.toFun (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            i) :
        β)),
  False
Tactic: refine (f.monotone ((p.monotone (Fin.le_last _)).trans hp)).lt_of_not_ge fun h'' ↦ ?_
-- 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 : α
n : ℕ
h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = (↑n : ℕ∞)
⊢ height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n : ℕ∞) + (↑m : ℕ∞)
have coe : ∀ (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 : ℕ∞)
Tactic: induction n using Nat.strong_induction_on generalizing x with | h n ih =>
    refine height_le_iff.mpr fun p hp ↦ le_of_not_gt fun h_len ↦ ?_
    let i : Fin (p.length + 1) := ⟨p.length - (m + 1), Nat.sub_lt_succ p.length _⟩
    suffices h'' : f (p i) < f x by
      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
      have h_lt : n' < n := ENat.coe_lt_coe.mp
        (h' ▸ hn' ▸ height_strictMono h'' (hn' ▸ ENat.coe_lt_top _))
      have := (length_le_height_last (p := p.take i)).trans <| ih n' h_lt (p i) hn'.symm
      rw [RelSeries.take_length, ENat.coe_sub, Nat.cast_add, Nat.cast_one, tsub_le_iff_right,
        add_assoc, add_comm _ (_ + 1), ← add_assoc, ← mul_add_one] at this
      refine not_lt_of_ge ?_ (h_len.trans_le this)
      gcongr
      rwa [← ENat.coe_one, ← ENat.coe_add, ENat.coe_le_coe]
    refine (f.monotone ((p.monotone (Fin.le_last _)).trans hp)).lt_of_not_ge fun h'' ↦ ?_
    let q' : LTSeries α := p.drop i
    let q : LTSeries (f ⁻¹' {f x}) := ⟨q'.length, fun j ↦ ⟨q' j, le_antisymm
      (f.monotone (le_trans (b := q'.last) (q'.monotone (Fin.le_last _)) (p.last_drop _ ▸ hp)))
      (le_trans (b := f q'.head) (p.head_drop _ ▸ h'')
        (f.monotone (q'.monotone (Fin.zero_le _))))⟩, fun i ↦ q'.step i⟩
    have := (LTSeries.length_le_krullDim q).trans (h (f x))
    simp only [RelSeries.drop_length, Nat.cast_le, tsub_le_iff_right, q', i, q] at this
    have : p.length > m := ENat.coe_lt_coe.mp ((le_add_left le_rfl).trans_lt h_len)
    lia
Cleared hypotheses: x, n, h'
-- 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 : α
n : ℕ∞
h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = n
⊢ height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * n + (↑m : ℕ∞)
have top : ∀ (h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = ⊤), height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * ⊤ + (↑m : ℕ∞)
Tactic: cases n with | top => simp | coe n =>
    induction n using Nat.strong_induction_on generalizing x with | h n ih =>
    refine height_le_iff.mpr fun p hp ↦ le_of_not_gt fun h_len ↦ ?_
    let i : Fin (p.length + 1) := ⟨p.length - (m + 1), Nat.sub_lt_succ p.length _⟩
    suffices h'' : f (p i) < f x by
      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
      have h_lt : n' < n := ENat.coe_lt_coe.mp
        (h' ▸ hn' ▸ height_strictMono h'' (hn' ▸ ENat.coe_lt_top _))
      have := (length_le_height_last (p := p.take i)).trans <| ih n' h_lt (p i) hn'.symm
      rw [RelSeries.take_length, ENat.coe_sub, Nat.cast_add, Nat.cast_one, tsub_le_iff_right,
        add_assoc, add_comm _ (_ + 1), ← add_assoc, ← mul_add_one] at this
      refine not_lt_of_ge ?_ (h_len.trans_le this)
      gcongr
      rwa [← ENat.coe_one, ← ENat.coe_add, ENat.coe_le_coe]
    refine (f.monotone ((p.monotone (Fin.le_last _)).trans hp)).lt_of_not_ge fun h'' ↦ ?_
    let q' : LTSeries α := p.drop i
    let q : LTSeries (f ⁻¹' {f x}) := ⟨q'.length, fun j ↦ ⟨q' j, le_antisymm
      (f.monotone (le_trans (b := q'.last) (q'.monotone (Fin.le_last _)) (p.last_drop _ ▸ hp)))
      (le_trans (b := f q'.head) (p.head_drop _ ▸ h'')
        (f.monotone (q'.monotone (Fin.zero_le _))))⟩, fun i ↦ q'.step i⟩
    have := (LTSeries.length_le_krullDim q).trans (h (f x))
    simp only [RelSeries.drop_length, Nat.cast_le, tsub_le_iff_right, q', i, q] at this
    have : p.length > m := ENat.coe_lt_coe.mp ((le_add_left le_rfl).trans_lt h_len)
    lia
Cleared hypotheses: n, h'