-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p₁ p₀ p₂ : PrimeSpectrum R
h₀_1 : p₀ < p₁
h₁_1 : p₁ < p₂
x : R
hx : x ∈ p₂.asIdeal
e : PrimeSpectrum (Localization.AtPrime p₂.asIdeal) ≃o
  (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ : PrimeSpectrum R }) : Type u_1) :=
  IsLocalization.AtPrime.primeSpectrumOrderIso (Localization.AtPrime p₂.asIdeal) p₂.asIdeal
hm :
  Eq.{u_1 + 1} (α := PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) (closedPoint (Localization.AtPrime p₂.asIdeal))
    ((e.symm :
        (a : (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1)) →
          PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
      (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
        x ∈ Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ : PrimeSpectrum R }) p₂ ⋯))
q : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)
hxq :
  Membership.mem (α := Localization.AtPrime p₂.asIdeal) (γ := Ideal (Localization.AtPrime p₂.asIdeal))
    (asIdeal
      ((e.symm :
          (a : (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1)) →
            PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
        ((e :
            (a : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) →
              (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1))
          q)))
    ((algebraMap R (Localization.AtPrime p₂.asIdeal) : (a : R) → Localization.AtPrime p₂.asIdeal) x :
      Localization.AtPrime p₂.asIdeal)
h₀ :
  LT.lt (α := PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
    ((e.symm :
          (a : (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1)) →
            PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
        (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
          x ∈ Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ : PrimeSpectrum R }) p₀ ⋯) :
      PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
    ((e.symm :
          (a : (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1)) →
            PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
        ((e :
            (a : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) →
              (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1))
          q) :
      PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
h₁ :
  LT.lt.{u_1} (α := Ideal (Localization.AtPrime p₂.asIdeal))
    (asIdeal
      ((e.symm :
          (a : (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1)) →
            PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
        ((e :
            (a : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) →
              (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1))
          q)))
    (maximalIdeal (Localization.AtPrime p₂.asIdeal))
hq :
  (↑((e :
            (a : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) →
              (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1))
          q) :
      PrimeSpectrum R) <
    p₂
⊢ ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q < p₂

Tactic:
exact Exists.intro (e q).1
    ⟨(p₂.1.under_map_of_isLocalizationAtPrime hq.le).le hxq, e.symm.lt_iff_lt.mp h₀, hq⟩

Premises used: Exists.intro, Subtype.val, DFunLike.coe