no goals
ι : Type u'
ι' : Type ?u.174501
R : Type u_1
K : Type ?u.174507
M : Type u_2
M' : Type ?u.174513
M'' : Type ?u.174516
V : Type u
V' : Type ?u.174521
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
⊢ ¬LinearIndependent R (v ∘ Subtype.val) ↔ ∃ f, f ∈ Finsupp.supported R R s ∧ ↑(Finsupp.total ι M R v) f = 0 ∧ f ≠ 0
simp [linearIndependent_comp_subtype, and_left_comm]