-- 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
i : ℕ
hi_1 :
  i <
    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
hi :
  i + 1 <
    q.length (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b}) +
      1
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (QuotSMulTop x M))
    (q.toFun (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      (⟨i + 1, hi⟩ :
        Fin
          (q.length (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b}) +
            1)))

Tactic:
simpa using
        ⟨mem_support_mono (by simpa [h0] using q.monotone (Fin.zero_le _)) p.head.2, q.monotone
          ((Fin.natCast_eq_mk (Nat.lt_of_add_left_lt hi)).trans_le (Nat.le_add_left 1 i)) hxq⟩