rw [Finsupp.total_apply, Finsupp.sum_of_support_subset _ Subset.rfl _ (by simp)] at hl0
case refine_1
α : 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 : (Finsupp.total ι M R f) l = 0
hls : ↑l.support ⊆ s
⊢ l = 0
case refine_1
α : 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 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
⊢ l = 0