rw [← finrank_top, ← hv]
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) = ⊤
⊢ finrank R M ≤ Fintype.card ι
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) = ⊤
⊢ finrank R ↥(Submodule.span R (Set.range v)) ≤ Fintype.card ι