simp
α : 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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
h : ∀ (l : ↑s →₀ R), (Finsupp.total (↑s) M R (s.restrict f)) l = 0 → l = 0
l : ι →₀ R
hl0 : (l.sum fun i a => a • f i) = 0
hls : ↑l.support ⊆ s
⊢ ∀ i ∈ l.support, 0 • f i = 0
no goals