-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
x : R
h : Membership.mem (γ := Ideal R) (Ideal.jacobson (annihilator R M)) x
h_1 : Nontrivial M
p : LTSeries (↑(support R M) : Type u_1)
hxp :
  x ∈
    (↑(RelSeries.last (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            p) :
        PrimeSpectrum R).asIdeal
q : LTSeries (PrimeSpectrum R)
hxq :
  x ∈
    (q.toFun (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        1).asIdeal
hq :
  RelSeries.length (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      (p.map
        (Subtype.val (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) x))
        ⋯) =
    q.length (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
h0 :
  (↑(RelSeries.head (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b})
          p) :
      PrimeSpectrum R) =
    RelSeries.head (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      q
right :
  RelSeries.last (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      (p.map
        (Subtype.val (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) x))
        ⋯) =
    RelSeries.last (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      q
hp0 :
  ¬p.length (r :=
        {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
          match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
          | (a, b) => a < b}) =
      0
q' : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) :=
  RelSeries.mk (r :=
    {x_1 :
      (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) × (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
      match (motive :=
        (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
            (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) →
          Prop)
        x_1 with
      | (a, b) => a < b})
    (p.length (r :=
        {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
          match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
          | (a, b) => a < b}) -
      1)
    (fun
        (h :
          Fin
            (p.length (r :=
                  {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                    match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1)) ↦
      match (motive :=
        Fin
            (p.length (r :=
                  {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                    match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                    | (a, b) => a < b}) -
                1 +
              1) →
          (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1))
        h with
      | ⟨i, hi⟩ =>
        have hi := ⋯;
        Subtype.mk (p := fun (x_1 : PrimeSpectrum R) ↦
          Membership.mem (γ := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (QuotSMulTop x M)) x_1)
          (q.toFun (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            ⟨i + 1, hi⟩)
          ⋯)
    ⋯
neg :
  (↑(p.length (r :=
              {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                | (a, b) => a < b}) -
            1 +
          1) :
      WithBot ℕ∞) ≤
    supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1
neg₁ :
  HAdd.hAdd (α := WithBot ℕ∞)
      (↑(p.length (r :=
              {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                | (a, b) => a < b}) -
            1) :
        WithBot ℕ∞)
      1 ≤
    supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1
neg₂ :
  HAdd.hAdd (α := WithBot ℕ∞)
      (↑(p.length (r :=
              {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                | (a, b) => a < b}) -
            1) :
        WithBot ℕ∞)
      1 ≤
    Order.krullDim.{u_1} (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) + 1
neg₃ :
  HAdd.hAdd (α := WithBot ℕ∞)
      (↑(p.length (r :=
              {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                | (a, b) => a < b}) -
            1) :
        WithBot ℕ∞)
      1 ≤
    HAdd.hAdd (α := WithBot ℕ∞)
      (⨆ (p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)),
        (↑(p.length (r :=
              {x_1 :
                (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                  (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
                match (motive :=
                  (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                      (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) →
                    Prop)
                  x_1 with
                | (a, b) => a < b})) :
          WithBot ℕ∞))
      1
neg₄ neg₅ :
  HAdd.hAdd (α := WithBot ℕ∞)
      (↑(p.length (r :=
              {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                | (a, b) => a < b}) -
            1) :
        WithBot ℕ∞)
      1 ≤
    HAdd.hAdd (α := WithBot ℕ∞)
      (↑(p.length (r :=
              {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                | (a, b) => a < b}) -
            1) :
        WithBot ℕ∞)
      1
⊢ (↑(p.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b})) :
      WithBot ℕ∞) ≤
    supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1

Tactic:
grw [le_tsub_add (b := p.length) (a := 1), Nat.cast_add_one, supportDim, Order.krullDim,
    ← le_iSup _ q']

Premises used: le_iSup, Order.krullDim, Module.supportDim, le_tsub_add, Nat.cast_add_one