rw [trace_quotient_eq_trace_localization_quotient S p Rₚ Sₚ, IsScalarTower.algebraMap_eq S Sₚ,
  RingHom.comp_apply, Ideal.Quotient.algebraMap_eq, Algebra.trace_quotient_mk,
  RingEquiv.apply_symm_apply, ← Algebra.intTrace_eq_trace,
  ← Algebra.intTrace_eq_of_isLocalization R S p.primeCompl (Aₘ := Rₚ) (Bₘ := Sₚ) x,
  ← Ideal.Quotient.algebraMap_eq, ← IsScalarTower.algebraMap_apply]
case 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.335608
Sₚ✝ : Type ?u.335611
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 (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : NoZeroSMulDivisors Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Module.Free Rₚ Sₚ
⊢ (equivQuotMaximalIdealOfIsLocalization p Rₚ) ((trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x)) =
    (equivQuotMaximalIdealOfIsLocalization p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))
case 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.335608
Sₚ✝ : Type ?u.335611
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 (algebraMapSubmonoid S p.primeCompl) Sₚ✝
inst✝⁶ : IsScalarTower R S Sₚ✝
inst✝⁵ : IsScalarTower R Rₚ✝ Sₚ✝
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : NoZeroSMulDivisors Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Module.Free Rₚ Sₚ
⊢ (algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) ((intTrace R S) x) =
    (equivQuotMaximalIdealOfIsLocalization p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))