simp only [leftMulMatrix_apply, coe_lmul_eq_mul, LinearMap.toMatrix_apply,
  basisQuotientOfLocalRing_apply, LinearMap.mul_apply', RingHom.toAddMonoidHom_eq_coe,
  AddMonoidHom.mapMatrix_apply, AddMonoidHom.coe_coe, Matrix.map_apply, ← map_mul,
  basisQuotientOfLocalRing_repr]
case e_A.a
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
i j : ι
⊢ (leftMulMatrix (basisQuotientOfLocalRing b)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) i j =
    (Ideal.Quotient.mk p).toAddMonoidHom.mapMatrix ((leftMulMatrix b) x) i j
no goals