no goals
R : Type u
M : Type v
N : Type w
inst✝¹⁰ : Ring R
inst✝⁹ : StrongRankCondition R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module.Free R M
inst✝⁵ : Module.Finite R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
ι : Type v
inst✝ : Fintype ι
⊢ finrank R (ι →₀ R) = card ι
rw [finrank, rank_finsupp_self, ← mk_toNat_eq_card, toNat_lift]