simp only [Quotient.mk_comp_algebraMap, Quotient.lift_mk, _root_.map_mul, AlgEquiv.commutes,
  RingHomCompTriple.comp_apply]
case map_smul'.intro
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
x : S₁ ⧸ comap e P
r : R
⊢ E ((Quotient.lift p ((Quotient.mk (comap e P)).comp (algebraMap R S₁)) ⋯) ((Quotient.mk p) r) * x) =
    (Quotient.lift p ((Quotient.mk P).comp (algebraMap R S₂)) ⋯) ((RingHom.id (R ⧸ p)) ((Quotient.mk p) r)) * E x
no goals