∀ {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (p : α → Prop) [inst_1 : DecidablePred p] (f g : α →₀ M),
  (fun f => ⇑f) (Finsupp.filter p (f + g)) = (fun f => ⇑f) (Finsupp.filter p f + Finsupp.filter p g)