no goals
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type ?u.355819
inst✝³ : AddCommGroup N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R M
⊢ trace R M = comp (contractLeft R M) ↑(LinearEquiv.symm (dualTensorHomEquivOfBasis b))
simp [LinearEquiv.eq_comp_toLinearMap_symm, trace_eq_contract_of_basis b]