∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddZeroClass (β i)] (p : ι → Prop) [inst_1 : DecidablePred p]
  (f g : Π₀ (i : ι), β i), DFinsupp.filter p (f + g) = DFinsupp.filter p f + DFinsupp.filter p g