awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.KrullDimension
Goal:
n : ℕ∞
top : height (α := ℕ∞) ⊤ = ⊤
coe : ∀ (n : ℕ), height (α := ℕ∞) (↑n : ℕ∞) = (↑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 _)

Premises used: Order.height_nat, Order.height_coe_withTop, Order.krullDim_enat, Order.height_top_eq_krullDim, WithBot.coe_top, WithBot.coe_eq_coe, Eq.trans
-- Module: Mathlib.Order.KrullDimension
Goal:
n : ℕ
apply : coheight n + 1 = ⊤
⊢ coheight (α := ℕ∞) (↑n : ℕ∞) = ⊤

Tactic:
apply (coheight_coe_withTop _).trans

Premises used: Order.coheight_coe_withTop, Eq.trans
-- Module: Mathlib.Order.KrullDimension
Goal:
n : ℕ
⊢ coheight n + 1 = ⊤

Tactic:
simp only [coheight_nat, top_add]

Premises used: Order.coheight_nat, top_add
-- Module: Mathlib.Order.KrullDimension
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 : α
generalize :
  ∀ (n : ℕ∞) (h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = n),
    height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * n + (↑m : ℕ∞)
⊢ height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * height.{u_2} (α := β) ((f : (a : α) → β) x : β) + (↑m : ℕ∞)

Tactic:
generalize h' : Order.height (f x) = n

Premises used: Order.height, DFunLike.coe
-- Module: Mathlib.Order.KrullDimension
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 : α
h' : height.{u_2} (α := β) ((f : (a : α) → β) x : β) = ⊤
⊢ height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * ⊤ + (↑m : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Order.KrullDimension
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 : ℕ∞)

Tactic:
height_le_iff.mpr fun p hp ↦ le_of_not_gt fun h_len ↦ ?_

Premises used: Iff.mpr, le_of_not_gt, Order.height_le_iff
-- Module: Mathlib.Order.KrullDimension
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 : ℕ∞)
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
⊢ height x ≤ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n : ℕ∞) + (↑m : ℕ∞)

Tactic:
refine height_le_iff.mpr fun p hp ↦ le_of_not_gt fun h_len ↦ ?_

Premises used: Iff.mpr, le_of_not_gt, Order.height_le_iff
-- Module: Mathlib.Order.KrullDimension
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' : ℕ),
    (↑n' : ℕ∞) =
      height.{u_2} (α := β)
        ((f : (a : α) → β)
            (p.toFun (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              i) :
          β)

Tactic:
ENat.ne_top_iff_exists.mp
        ((height_mono h''.le).trans_lt (h' ▸ ENat.coe_lt_top _)).ne

Premises used: ENat.ne_top_iff_exists, LT.lt.le, Iff.mp, Order.height_mono, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.Order.KrullDimension
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 : β)
obtain :
  ∀ (n' : ℕ)
    (hn' :
      (↑n' : ℕ∞) =
        height.{u_2} (α := β)
          ((f : (a : α) → β)
              (p.toFun (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                i) :
            β)),
    False
⊢ 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

Premises used: ENat.ne_top_iff_exists, LT.lt.le, Iff.mp, RelSeries.toFun, Order.height_mono, Order.height, LE.le.trans_lt, DFunLike.coe, LT.lt.ne
-- Module: Mathlib.Order.KrullDimension
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) :
        β)
⊢ n' < n

Tactic:
have h_lt : n' < n := ENat.coe_lt_coe.mp
        (h' ▸ hn' ▸ height_strictMono h'' (hn' ▸ ENat.coe_lt_top _))
-- Module: Mathlib.Order.KrullDimension
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
⊢ (↑((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
-- Module: Mathlib.Order.KrullDimension
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 : ℕ∞)
⊢ (↑(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

Premises used: add_assoc, RelSeries.take_length, tsub_le_iff_right, add_comm, Nat.cast_add, ENat.coe_sub, HAdd.hAdd, mul_add_one, OfNat.ofNat, Nat.cast_one
-- Module: Mathlib.Order.KrullDimension
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

Tactic:
not_lt_of_ge ?_ (h_len.trans_le this)

Premises used: LT.lt.trans_le, not_lt_of_ge
-- Module: Mathlib.Order.KrullDimension
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 : ℕ∞)
refine :
  HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * HAdd.hAdd (α := ℕ∞) (↑n' : ℕ∞) 1 + (↑m : ℕ∞) ≤
    HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n : ℕ∞) + (↑m : ℕ∞)
⊢ False

Tactic:
refine not_lt_of_ge ?_ (h_len.trans_le this)

Premises used: LT.lt.trans_le, not_lt_of_ge
-- Module: Mathlib.Order.KrullDimension
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 (α := ℕ∞) (↑m : ℕ∞) 1 * HAdd.hAdd (α := ℕ∞) (↑n' : ℕ∞) 1 + (↑m : ℕ∞) ≤
    HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) 1 * (↑n : ℕ∞) + (↑m : ℕ∞)

Tactic:
gcongr
-- Module: Mathlib.Order.KrullDimension
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 : ℕ∞)
bc₂ bc₃ bc₄ bc₅ : n' + 1 ≤ n
⊢ HAdd.hAdd (α := ℕ∞) (↑n' : ℕ∞) 1 ≤ (↑n : ℕ∞)

Tactic:
rwa [← ENat.coe_one, ← ENat.coe_add, ENat.coe_le_coe]

Premises used: ENat.coe_one, ENat.coe_le_coe, ENat.coe_add
-- Module: Mathlib.Order.KrullDimension
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),
    ⋯⟩
coe :
  LT.lt.{u_2} (α := β)
    ((f : (a : α) → β)
        (p.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i) :
      β)
    ((f : (a : α) → β) x : β)
⊢ False

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]