-- 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 :
      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)),
    Membership.mem (α :=
      (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) × (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1))
      (γ :=
      SetRel (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
        (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1))
      {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}
      ((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))
            i.castSucc 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⟩)
              ⋯,
          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))
            i.succ 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⟩)
              ⋯) :
        (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) × (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1))

Tactic:
exact fun _ ↦ q.strictMono (by simp)

Premises used: LTSeries.strictMono