-- 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
⊢ Eq.{u_4 + 1} (α :=
    HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@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ₚ))
            (Ideal.Quotient.mk p) :
          (a : R) → Sₚ ⧸ pSₚ)
        x :
      HasQuotient.Quotient Sₚ (B := Ideal Sₚ) (Ideal.map (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)))
    (((RingHom.comp
              (@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))))
              (Ideal.Quotient.mk p) :
            RingHom.{u_1, u_4} 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ₚ)))
have he : 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ₚ)))
Tactic: simp only [equivQuotMaximalIdeal, RingHom.quotientKerEquivOfSurjective,
      RingEquiv.coe_ringHom_trans, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply,
      Ideal.quotEquivOfEq_mk, RingHom.quotientKerEquivOfRightInverse.apply, RingHom.kerLift_mk,
      equivQuotientMapMaximalIdeal, Ideal.Quotient.algebraMap_quotient_map_quotient]