no goals
R : Type u_1
inst✝⁹ : CommRing R
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type ?u.396174
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type ?u.396716
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
⊢ ↑(trace R M) id = ↑(finrank R M)
rw [← one_eq_id, trace_one]