no goals
α : Type u_1
β : Type ?u.358141
γ : Type ?u.358144
ι : Type ?u.358147
M : Type u_2
M' : Type ?u.358153
N : Type ?u.358156
P : Type ?u.358159
G : Type ?u.358162
H : Type ?u.358165
R : Type ?u.358168
S : Type ?u.358171
inst✝ : Zero M
p : α → Prop
f : α →₀ M
⊢ filter p f = 0 ↔ ∀ (x : α), p x → ↑f x = 0
simp only [FunLike.ext_iff, filter_eq_indicator, zero_apply, Set.indicator_apply_eq_zero,
  Set.mem_setOf_eq]