Restriction of a sum ignoring zeros

Stream: Is there code for X?

[Adam Topaz]

Does anyone know of an efficient way to prove the following?

import algebra.big_operators

open_locale big_operators

example {ι M : Type*}
  [add_comm_monoid M] [fintype ι] (m : ι → M)
  (S : finset ι) (hS : ∀ i, i ∉ S → m i = 0) :
  (∑ i, m i) = (∑ i in S, m i) := sorry

[Eric Wieser]

docs#finset.sum_subset should get you most of the way there

[Adam Topaz]

Ah perfect, thanks!

[Eric Wieser]

You just have to eliminate the \mem univ it produces

[Adam Topaz]

right, yeah that lemma is exactly what I need

[Junyan Xu]

I found docs#finset.sum_add_sum_compl and docs#finset.sum_eq_zero but that seems less direct.