rw [Module.rank_def] at 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 : Module.rank R M = ↑(finrank R M)
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
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