classical
let ι := Module.Free.ChooseBasisIndex R S
let b : Basis ι R S := Module.Free.chooseBasis R S
rw [trace_eq_matrix_trace b, trace_eq_matrix_trace (basisQuotientOfLocalRing b)]
show _ = (Ideal.Quotient.mk p).toAddMonoidHom _
rw [AddMonoidHom.map_trace]
congr 1
ext i j
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]
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
⊢ (trace (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) =
    (Ideal.Quotient.mk p) ((trace R S) x)
no goals