rw [Finsupp.extendDomain_eq_embDomain_subtype, Finsupp.total_embDomain] at h
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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ↑s →₀ R
hl0 : (Finsupp.total (↑s) M R (s.restrict f)) l = 0
h : (Finsupp.total ι M R f) l.extendDomain = 0 → ↑l.extendDomain.support ⊆ s → l.extendDomain = 0
⊢ l = 0
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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ↑s →₀ R
hl0 : (Finsupp.total (↑s) M R (s.restrict f)) l = 0
h :
  (Finsupp.total { x // x ∈ s } M R (f ∘ ⇑(Embedding.subtype fun x => x ∈ s))) l = 0 →
    ↑(Finsupp.embDomain (Embedding.subtype fun x => x ∈ s) l).support ⊆ s →
      Finsupp.embDomain (Embedding.subtype fun x => x ∈ s) l = 0
⊢ l = 0