-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
x : R
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}) =
    0
h :
  x ∈
      (RelSeries.toFun (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          (RelSeries.singleton
            {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})
              p))
          1).asIdeal ∧
    0 =
        RelSeries.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          (RelSeries.singleton
            {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})
              p)) ∧
      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})
            (RelSeries.singleton
              {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})
                p)) ∧
        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})
            (RelSeries.singleton
              {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})
                p))
⊢ ∃ (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 ∧
      0 =
          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:
use RelSeries.singleton _ p.last

Premises used: RelSeries.last, RelSeries.singleton