Theorem: Finsupp.mul_filter' (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝³ : Monad m
ι : Type u_2
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
β : Type u_1
inst✝ : MulZeroClass β
f g : ι →₀ β
⊢ filter P (f * g) = filter P f * filter P g
Tactic:
simp [Finsupp.mul_filter]
State after:
no goals