no goals
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : StrongRankCondition K
ι : Type w
b : Finset ι
h : Basis { x // x ∈ b } K V
⊢ finrank K V = Finset.card b
rw [finrank_eq_card_basis h, Fintype.card_coe]