-- Module: Mathlib.RingTheory.Localization.AtPrime.Extension
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ₚ
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))))
⊢ 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)

Tactic:
obtain ⟨x, s, rfl⟩ := mk'_surjective p.primeCompl x

Premises used: IsLocalization.mk'_surjective, Ideal.primeCompl, rfl