-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (goal)
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))
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))
        ((e :
            (a : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) →
              (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1))
          q) :
      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))
rwa :
  ∀
    (h :
      LT.lt (α := (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ : PrimeSpectrum R }) : Type u_1))
        ((e :
              (a : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) →
                (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1))
            q :
          (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ : PrimeSpectrum R }) : Type u_1))
        (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
            x ∈ Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ : PrimeSpectrum R }) p₂ ⋯ :
          { x : PrimeSpectrum R // x ∈ Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ : PrimeSpectrum R } })),
    (↑((e :
              (a : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) →
                (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1))
            q) :
        PrimeSpectrum R) <
      p₂
⊢ (↑((e :
            (a : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) →
              (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1))
          q) :
      PrimeSpectrum R) <
    p₂
have rwa₁ : ∀
  (h :
    (↑((e :
              (a : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) →
                (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := sorry }) : Type u_1))
            q) :
        PrimeSpectrum R) <
      p₂),
  (↑((e :
            (a : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) →
              (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := sorry }) : Type u_1))
          q) :
      PrimeSpectrum R) <
    p₂
Tactic: rwa [OrderIso.lt_iff_lt, Subtype.mk_lt_mk] at h
Cleared hypotheses: h