ext x
case he
R : Type u_1
S : Type u_2
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
p : Ideal R
inst✝¹² : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : IsLocalization.AtPrime Rₚ p
inst✝⁷ : LocalRing Rₚ
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
⊢ (algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)).comp ↑(equivQuotMaximalIdealOfIsLocalization p Rₚ) =
    (↑(quotMapEquivQuotMapMaximalIdealOfIsLocalization S p Rₚ Sₚ)).comp (algebraMap (R ⧸ p) (S ⧸ pS))
case he.h.a
R : Type u_1
S : Type u_2
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
p : Ideal R
inst✝¹² : p.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : CommRing Sₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : IsLocalization.AtPrime Rₚ p
inst✝⁷ : LocalRing Rₚ
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
x✝ : S
this : IsScalarTower R (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)
x : R
⊢ (((algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)).comp ↑(equivQuotMaximalIdealOfIsLocalization p Rₚ)).comp
        (Ideal.Quotient.mk p))
      x =
    (((↑(quotMapEquivQuotMapMaximalIdealOfIsLocalization S p Rₚ Sₚ)).comp (algebraMap (R ⧸ p) (S ⧸ pS))).comp
        (Ideal.Quotient.mk p))
      x