no goals
R : Type u_1
inst✝¹³ : CommRing R
M : Type u_2
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
N : Type ?u.770483
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : Module R N
ι : Type ?u.771025
inst✝⁸ : Module.Free R M
inst✝⁷ : Module.Finite R M
inst✝⁶ : Module.Free R N
inst✝⁵ : Module.Finite R N
inst✝⁴ : Nontrivial R
p : Submodule R M
f : M →ₗ[R] M
h : IsProj p f
inst✝³ : Module.Free R { x // x ∈ p }
inst✝² : Module.Finite R { x // x ∈ p }
inst✝¹ : Module.Free R { x // x ∈ ker f }
inst✝ : Module.Finite R { x // x ∈ ker f }
⊢ ↑(LinearMap.trace R M) f = ↑(finrank R { x // x ∈ p })
rw [h.eq_conj_prodMap, trace_conj', trace_prodMap', trace_id, map_zero, add_zero]