obtain ⟨⟨s, hs⟩, hι : #s = _⟩ :=
  Cardinal.exists_eq_natCast_of_iSup_eq _ (Cardinal.bddAbove_range.{v, v} _) _ this
case neg
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, s.card = finrank R M ∧ LinearIndependent R Subtype.val
case neg.intro.mk
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)
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val