-- Lean 4 proof step from Mathlib.RingTheory.Trace.Quotient (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.IsMaximal
Rₚ : Type u_3
Sₚ : Type u_4
inst_4 : CommRing Rₚ
inst_5 : CommRing Sₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization.AtPrime Rₚ p
inst_8 : IsLocalRing Rₚ
inst_9 : Algebra S Sₚ
inst_10 : Algebra R Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_13 : IsScalarTower R S Sₚ
inst_14 : IsScalarTower R Rₚ Sₚ
x : S
this :
  IsScalarTower.{u_1, u_3, u_4} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
    (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
⊢ Eq.{u_1 + 1} (α := R ⧸ p)
    ((Algebra.trace (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :
          (a : S ⧸ pS) → R ⧸ p)
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
      R ⧸ 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)
        ((Algebra.trace (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
            (a : Sₚ ⧸ pSₚ) → Rₚ ⧸ maximalIdeal Rₚ)
          ((algebraMap S
                (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                  (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
              (a : S) → Sₚ ⧸ pSₚ)
            x)) :
      R ⧸ p)
have rw : Eq.{u_1 + 1} (α := R ⧸ 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)
      ((Algebra.trace (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
            (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
              (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
          (a : Sₚ ⧸ pSₚ) → Rₚ ⧸ maximalIdeal Rₚ)
        (((equivQuotientMapMaximalIdeal S p Rₚ Sₚ :
              RingEquiv.{u_2, u_4} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
                (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                  (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))) :
            (a : S ⧸ pS) → Sₚ ⧸ pSₚ)
          ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x))) :
    R ⧸ 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)
      ((Algebra.trace (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
            (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
              (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
          (a : Sₚ ⧸ pSₚ) → Rₚ ⧸ maximalIdeal Rₚ)
        ((algebraMap S
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
            (a : S) → Sₚ ⧸ pSₚ)
          x)) :
    R ⧸ p)
Tactic: rw [Algebra.trace_eq_of_equiv_equiv (equivQuotMaximalIdeal p Rₚ)
    (equivQuotientMapMaximalIdeal S p Rₚ Sₚ)]