no goals
R : Type u_1
inst✝⁹ : CommRing R
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type ?u.575799
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type ?u.576341
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
f : M →ₗ[R] M
⊢ ↑(trace R (Module.Dual R M)) (↑Module.Dual.transpose f) = ↑(trace R M) f
rw [← comp_apply, trace_transpose]