no goals
α : Type u_1
β : Type ?u.397891
γ : Type ?u.397894
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ a ∈ filter (fun a => ¬p a) s ↔ a ∈ s \ filter p s
simp only [Bool.decide_coe, Bool.not_eq_true', mem_filter, and_comm, mem_sdiff, not_and_or,
  Bool.not_eq_true, and_or_left, and_not_self, or_false]