-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Extension (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
Rₚ : Type u_3
inst_4 : CommRing Rₚ
inst_5 : Algebra R Rₚ
inst_6 : IsLocalization.AtPrime Rₚ p
inst_7 : IsLocalRing Rₚ
Sₚ : Type u_4
inst_8 : CommRing Sₚ
inst_9 : Algebra S Sₚ
inst_10 : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst_11 : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst_12 : Algebra R Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
inst_15 : p.IsMaximal
inst_16 : P.IsMaximal
inst_17 : LiesOver.{u_3, u_4} (B := Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P) (maximalIdeal Rₚ)
x : Rₚ
⊢ Eq.{u_2 + 1} (α := S ⧸ P)
    ((algebraMap (R ⧸ p) (S ⧸ P) : (a : R ⧸ p) → S ⧸ P)
        (((RingEquiv.symm (equivQuotMaximalIdeal p Rₚ) :
              RingEquiv.{u_3, u_1} (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) (R ⧸ p)) :
            (a : Rₚ ⧸ maximalIdeal Rₚ) → R ⧸ p)
          ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ) x)) :
      S ⧸ P)
    (((RingEquiv.symm (equivQuotientMapOfIsMaximal p Sₚ P) :
            RingEquiv.{u_4, u_2}
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) (S ⧸ P)) :
          (a : Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P) → S ⧸ P)
        ((algebraMap (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
            (a : Rₚ ⧸ maximalIdeal Rₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
          ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ) x)) :
      S ⧸ P)
have obtain : ∀ (x : R × ↥p.primeCompl),
  Eq.{u_2 + 1} (α := S ⧸ P)
    ((algebraMap (R ⧸ p) (S ⧸ P) : (a : R ⧸ p) → S ⧸ P)
      (((RingEquiv.symm (equivQuotMaximalIdeal p Rₚ) :
            RingEquiv.{u_3, u_1} (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) (R ⧸ p)) :
          (a : Rₚ ⧸ maximalIdeal Rₚ) → R ⧸ p)
        ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ)
          ((fun (x : R × ↥p.primeCompl) ↦
              (match (motive := R × ↥p.primeCompl → Rₚ) x with
                | (r, m) => mk' Rₚ r m :
                Rₚ))
            x))))
    (((RingEquiv.symm (equivQuotientMapOfIsMaximal p Sₚ P) :
          RingEquiv.{u_4, u_2} (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P))
            (S ⧸ P)) :
        (a : Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P) → S ⧸ P)
      ((algebraMap (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
            (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := S →+* Sₚ) (algebraMap S Sₚ) P)) :
          (a : Rₚ ⧸ maximalIdeal Rₚ) → Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)
        ((Ideal.Quotient.mk (maximalIdeal Rₚ) : (a : Rₚ) → Rₚ ⧸ maximalIdeal Rₚ)
          ((fun (x : R × ↥p.primeCompl) ↦
              (match (motive := R × ↥p.primeCompl → Rₚ) x with
                | (r, m) => mk' Rₚ r m :
                Rₚ))
            x))))
Tactic: obtain ⟨x, s, rfl⟩ := mk'_surjective p.primeCompl x
Cleared hypotheses: x