simp [hc' x hx]
α : 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 : ι
x✝ : x ∈ Finset.univ
hx : x ∉ s
⊢ c x • f x = 0
no goals