no goals
α : Type u_1
β : Type ?u.398605
γ : Type ?u.398608
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s₁ s₂ : Finset α
x✝ : α
⊢ x✝ ∈ s₁ \ s₂ ↔ x✝ ∈ filter (fun x => ¬x ∈ s₂) s₁
simp [mem_sdiff, mem_filter]