simp only [Finsupp.total_comapDomain, restrict_apply] at h
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
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
h :
  (Finsupp.total (↑s) M R (s.restrict f)) (Finsupp.comapDomain Subtype.val l ⋯) = 0 →
    Finsupp.comapDomain Subtype.val l ⋯ = 0
⊢ 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
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
h : ∑ x ∈ l.support.preimage Subtype.val ⋯, l ↑x • f ↑x = 0 → Finsupp.comapDomain Subtype.val l ⋯ = 0
⊢ l = 0