This provides lemmas about sets (mostly dealing with disjointness) that are missing in Mathlib. We do not use out custom notation here because this file is higher than Basic.lean in the import hierarchy.

theorem setminus_inter_union_eq_union {α : Type u_1} {X : Set α} {Y : Set α} : X \ (X ∩ Y) ∪ Y = X ∪ Y

theorem Disjoint.ni_of_in {α : Type u_1} {X : Set α} {Y : Set α} {a : α} (hXY : Disjoint X Y) (ha : a ∈ X) : a ∉ Y

theorem disjoint_of_singleton_intersection_left_wo {α : Type u_1} {X : Set α} {Y : Set α} {a : α} (hXY : X ∩ Y = {a}) : Disjoint (X \ {a}) Y

theorem disjoint_of_singleton_intersection_right_wo {α : Type u_1} {X : Set α} {Y : Set α} {a : α} (hXY : X ∩ Y = {a}) : Disjoint X (Y \ {a})

theorem disjoint_of_singleton_intersection_both_wo {α : Type u_1} {X : Set α} {Y : Set α} {a : α} (hXY : X ∩ Y = {a}) : Disjoint (X \ {a}) (Y \ {a})