feat: s \ {a ∈ s | p a} = {a ∈ s | ¬ p a} (#24888)

I wrote this for #22974, but it isn't needed there in the end.

Author: YaelDillies

Mathlib/Data/Set/Basic.lean

@@ -1238,6 +1238,9 @@ theorem diff_diff_cancel_left {s t : Set α} (h : s ⊆ t) : t \ (t \ s) = s :=
 theorem union_eq_diff_union_diff_union_inter (s t : Set α) : s ∪ t = s \ t ∪ t \ s ∪ s ∩ t :=
   sup_eq_sdiff_sup_sdiff_sup_inf
 
+@[simp] lemma sdiff_sep_self (s : Set α) (p : α → Prop) : s \ {a ∈ s | p a} = {a ∈ s | ¬ p a} :=
+  diff_self_inter
+
 /-! ### Powerset -/
 
 theorem mem_powerset {x s : Set α} (h : x ⊆ s) : x ∈ 𝒫 s := @h