-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (hypothesis)
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))
⊢ ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q < p₂
have hq : (↑((e :
          (a : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) →
            (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := sorry }) : Type u_1))
        q) :
    PrimeSpectrum R) <
  p₂
Tactic: have hq : (e q).1 < p₂ := by
    have h : e.symm (e q) < e.symm ⟨p₂, le_refl p₂⟩ :=
      h₁.trans_eq Localization.AtPrime.map_eq_maximalIdeal.symm
    rwa [OrderIso.lt_iff_lt, Subtype.mk_lt_mk] at h