no goals
R : Type u_1
inst✝⁹ : CommRing R
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type u_3
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type ?u.740490
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
e : M ≃ₗ[R] N
⊢ ↑(trace R N) (↑(LinearEquiv.conj e) f) = ↑(trace R M) f
rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe,
  LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, id_comp]