∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M)
  [inst_2 : CommMonoid N] (g : α → M → N), (Finsupp.filter p f).prod g = ∏ x ∈ (Finsupp.filter p f).support, g x (f x)