-- 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'' :
  LE.le.{u_2} (α := β) ((f : (a : α) → β) x : β)
    ((f : (a : α) → β)
        (p.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i) :
      β)
q' : LTSeries α :=
  RelSeries.drop (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a < b})
    p i
q : LTSeries (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) : Type u_1) :=
  RelSeries.mk (r :=
    {x_1 :
      (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) : Type u_1) ×
        (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) : Type u_1) |
      match (motive :=
        (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) : Type u_1) ×
            (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) : Type u_1) →
          Prop)
        x_1 with
      | (a, b) => a < b})
    (q'.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}))
    (fun
        (j :
          Fin
            (q'.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) +
              1)) ↦
      Subtype.mk (p := fun (x_1 : α) ↦
        Membership.mem (γ := Set α)
          (Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) x_1)
        (q'.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          j)
        ⋯)
    ⋯
this :
  LE.le (α := WithBot ℕ∞)
    (↑(q.length (r :=
          {x_1 :
            (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) : Type u_1) ×
              (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) : Type u_1) |
            match (motive :=
              (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) : Type u_1) ×
                  (↑(Set.preimage (β := β) (⇑f : (a : α) → β) (singleton (α := β) ((f : (a : α) → β) x : β))) :
                    Type u_1) →
                Prop)
              x_1 with
            | (a, b) => a < b})) :
      WithBot ℕ∞)
    (↑m : WithBot ℕ∞)
⊢ p.length (r := {x : α × α | x.1 < x.2}) ≤ m + (p.length (r := {x : α × α | x.1 < x.2}) - (m + 1))

Tactic:
simp only [RelSeries.drop_length, Nat.cast_le, tsub_le_iff_right, q', i, q] at this

Premises used: tsub_le_iff_right, Nat.cast_le, RelSeries.drop_length