no goals
α : Type u_1
β : Type ?u.425326
γ : Type ?u.425329
ι : Type ?u.425332
M : Type u_2
M' : Type ?u.425338
N : Type ?u.425341
P : Type ?u.425344
G : Type ?u.425347
H : Type ?u.425350
R : Type ?u.425353
S : Type ?u.425356
inst✝ : Zero M
p : α → Prop
f : α →₀ M
⊢ filter p f = f ↔ ∀ (x : α), ↑f x ≠ 0 → p x
simp only [FunLike.ext_iff, filter_eq_indicator, Set.indicator_apply_eq_self, Set.mem_setOf_eq,
  not_imp_comm]