no goals
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.355098
R : Type u
inst✝³ : Ring R
inst✝² : StrongRankCondition R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
v : ι → M
i : LinearIndependent R v
w : Finset M
s : span R ↑w = ⊤
⊢ (#ι) ≤ ↑(Finset.card w)
simpa only [Finset.coe_sort_coe, Fintype.card_coe] using linearIndependent_le_span v i w s