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.570799
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
s : Finset V
⊢ (#↑↑s) = ↑(Finset.card s)
rw [Finset.coe_sort_coe, Cardinal.mk_coe_finset]