by_cases H : finrank R M = 0
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
case pos
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : finrank R M = 0
⊢ ∃ 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
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val