rwa [s.sum_attach (fun x ↦ c x • f x),
  Finset.sum_subset (s.subset_univ) (fun x _ hx ↦ by simp [hc' x hx])]
case refine_2
α : 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
x✝ : ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
c : ι → R
hc0 : ∑ i : ι, c i • f i = 0
b : ι
hbs : b ∈ s
hb0 : ¬c b = 0
hc' : ∀ i ∉ s, c i = 0
⊢ ∑ x ∈ s.attach, c ↑x • f ↑x = 0
no goals