-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R))
    (hx :
      x ∈
        (RelSeries.last (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            p).asIdeal)
    (hp :
      p.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b}) =
        n),
    ∃ (q : LTSeries (PrimeSpectrum R)),
      x ∈
          (q.toFun (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})
              1).asIdeal ∧
        n =
            q.length (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b}) ∧
          RelSeries.head (r :=
                {x : PrimeSpectrum R × PrimeSpectrum R |
                  match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                  | (a, b) => a < b})
                p =
              RelSeries.head (r :=
                {x : PrimeSpectrum R × PrimeSpectrum R |
                  match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                  | (a, b) => a < b})
                q ∧
            RelSeries.last (r :=
                {x : PrimeSpectrum R × PrimeSpectrum R |
                  match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                  | (a, b) => a < b})
                p =
              RelSeries.last (r :=
                {x : PrimeSpectrum R × PrimeSpectrum R |
                  match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                  | (a, b) => a < b})
                q
p : LTSeries (PrimeSpectrum R)
hx :
  x ∈
    (RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        p).asIdeal
hp :
  p.length (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b}) =
    n + 1
h0 : ¬n = 0
q : PrimeSpectrum R
hxq : x ∈ q.asIdeal
h2 :
  p.toFun (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      (⟨p.length (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b}) -
            2,
          ⋯⟩ :
        Fin
          (p.length (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b}) +
            1)) <
    q
hq :
  q <
    RelSeries.last (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      p
neg :
  ∀ (Q : LTSeries (PrimeSpectrum R))
    (hx :
      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 :
      n =
        Q.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b}))
    (hh :
      ((RelSeries.eraseLast (r :=
                      {x : PrimeSpectrum R × PrimeSpectrum R |
                        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                        | (a, b) => a < b})
                      p).eraseLast
                  (r :=
                  {x : PrimeSpectrum R × PrimeSpectrum R |
                    match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                    | (a, b) => a < b}).snoc
              (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})
              q h2).head
          (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b}) =
        RelSeries.head (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          Q)
    (hl :
      ((RelSeries.eraseLast (r :=
                      {x : PrimeSpectrum R × PrimeSpectrum R |
                        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                        | (a, b) => a < b})
                      p).eraseLast
                  (r :=
                  {x : PrimeSpectrum R × PrimeSpectrum R |
                    match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                    | (a, b) => a < b}).snoc
              (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})
              q h2).last
          (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b}) =
        RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          Q),
    ∃ (q : LTSeries (PrimeSpectrum R)),
      x ∈
          (q.toFun (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})
              1).asIdeal ∧
        n + 1 =
            q.length (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b}) ∧
          RelSeries.head (r :=
                {x : PrimeSpectrum R × PrimeSpectrum R |
                  match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                  | (a, b) => a < b})
                p =
              RelSeries.head (r :=
                {x : PrimeSpectrum R × PrimeSpectrum R |
                  match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                  | (a, b) => a < b})
                q ∧
            RelSeries.last (r :=
                {x : PrimeSpectrum R × PrimeSpectrum R |
                  match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                  | (a, b) => a < b})
                p =
              RelSeries.last (r :=
                {x : PrimeSpectrum R × PrimeSpectrum R |
                  match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                  | (a, b) => a < b})
                q
⊢ ∃ (q : LTSeries (PrimeSpectrum R)),
    x ∈
        (q.toFun (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            1).asIdeal ∧
      n + 1 =
          q.length (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b}) ∧
        RelSeries.head (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})
              p =
            RelSeries.head (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})
              q ∧
          RelSeries.last (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})
              p =
            RelSeries.last (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})
              q

Tactic:
obtain ⟨Q, hx, hQ, hh, hl⟩ := hn (p.eraseLast.eraseLast.snoc q h2) (by simpa using hxq) <| by
    simpa [hp] using Nat.succ_pred_eq_of_ne_zero h0

Premises used: RelSeries.eraseLast, RelSeries.snoc