convert Fintype.card_range_le v
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
ι : Type u_3
inst✝ : Fintype ι
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ (Set.range v).toFinset.card ≤ Fintype.card ι
case h.e'_3
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
ι : Type u_3
inst✝ : Fintype ι
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ (Set.range v).toFinset.card = Fintype.card ↑(Set.range v)