simp only [Finset.coe_sort_coe, not_linearIndependent_iff, Finset.univ_eq_attach, restrict_apply,
  ne_eq, Subtype.exists, Finset.mem_coe]
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
⊢ ¬LinearIndependent (ι := ↑↑s) R ((↑s).restrict f) ↔
    ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, c i ≠ 0) ∧ ∀ i ∉ s, c i = 0
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
⊢ (∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0) ↔
    ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0