-- 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ₚ)))
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)
⊢ 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 he : Eq (α :=
  RingHom.{u_1, u_4} (R ⧸ p)
    (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (algebraMap (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))
      (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))))
    (↑(equivQuotMaximalIdeal p Rₚ) : R ⧸ p →+* Rₚ ⧸ maximalIdeal Rₚ))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(equivQuotientMapMaximalIdeal S p Rₚ Sₚ) : S ⧸ pS →+* Sₚ ⧸ pSₚ)
    (algebraMap (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))))
Tactic: rw [Algebra.trace_eq_of_equiv_equiv (equivQuotMaximalIdeal p Rₚ)
    (equivQuotientMapMaximalIdeal S p Rₚ Sₚ)]