exact ⟨s.toFinset,
  Cardinal.natCast_injective (by rwa [Set.toFinset_card, ← Cardinal.mk_fintype]),
  by convert hs <;> simp only [Set.mem_toFinset]⟩
case neg.intro.mk.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝¹ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this✝ : ⨆ ι, #↑↑ι = ↑(finrank R M)
s : Set M
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
hι : #↑s = ↑(finrank R M)
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
no goals