-- 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_1 : 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ₚ)))
x : R
he :
  Eq.{u_4 + 1} (α :=
    HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
    ((algebraMap R
            (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
              (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
          (a : R) → Sₚ ⧸ pSₚ)
        x :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
    (((algebraMap S
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
            RingHom.{u_2, u_4} S
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))) :
          (a : S) → Sₚ ⧸ pSₚ)
        ((algebraMap R S : (a : R) → S) x) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
⊢ Eq.{u_4 + 1} (α :=
    HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
    ((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ₚ))) :
          (a : Rₚ ⧸ maximalIdeal Rₚ) → Sₚ ⧸ pSₚ)
        (((algebraMap R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ)) :
              RingHom.{u_1, u_3} R (HasQuotient.Quotient Rₚ (B := Ideal Rₚ) (maximalIdeal Rₚ))) :
            (a : R) → Rₚ ⧸ maximalIdeal Rₚ)
          x) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
    (((algebraMap S
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
            RingHom.{u_2, u_4} S
              (HasQuotient.Quotient Sₚ (B := Ideal Sₚ)
                (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))) :
          (a : S) → Sₚ ⧸ pSₚ)
        ((algebraMap R S : (a : R) → S) x) :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
have he₁ : Eq.{u_4 + 1} (α :=
  HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
  ((algebraMap R
          (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
        (a : R) → Sₚ ⧸ pSₚ)
      x :
    HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
  ((algebraMap R
          (HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ))) :
        (a : R) → Sₚ ⧸ pSₚ)
      x :
    HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
Tactic: rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]