This provides lemmas about sets (mostly dealing with disjointness) that are missing in Mathlib.

theorem set_union_union_eq_rev {α : Type} (X Y Z : Set α) : X ∪ Y ∪ Z = Z ∪ Y ∪ X

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

theorem nonempty_inter_not_ssubset_empty_inter {α : Type} {A B E : Set α} (hA : (A ∩ E).Nonempty) (hB : B ∩ E = ∅) : ¬A ⊂ B

theorem ssubset_self_union_other_elem {α : Type} {a : α} {X : Set α} (ha : a ∉ X) : X ⊂ X ∪ {a}

theorem singleton_union_ssubset_union_iff {α : Type} {a : α} {A B : Set α} (haA : a ∉ A) (haB : a ∉ B) : A ∪ {a} ⊂ B ∪ {a} ↔ A ⊂ B

theorem ssub_parts_ssub {α : Type} {A B E₁ E₂ : Set α} (hA : A ⊆ E₁ ∪ E₂) (hB : B ⊆ E₁ ∪ E₂) (hAB₁ : A ∩ E₁ ⊂ B ∩ E₁) (hAB₂ : A ∩ E₂ ⊂ B ∩ E₂) : A ⊂ B

theorem HasSubset.Subset.parts_eq {α : Type} {A E₁ E₂ : Set α} (hA : A ⊆ E₁ ∪ E₂) : A ∩ E₁ ∪ A ∩ E₂ = A

theorem elem_notin_set_minus_singleton {α : Type} (a : α) (X : Set α) : a ∉ X \ {a}

theorem sub_union_diff_sub_union {α : Type} {A B C : Set α} (hA : A ⊆ B \ C) : A ⊆ B

theorem singleton_inter_in_left {α : Type} {X Y : Set α} {a : α} (ha : X ∩ Y = {a}) : a ∈ X

theorem singleton_inter_in_right {α : Type} {X Y : Set α} {a : α} (ha : X ∩ Y = {a}) : a ∈ Y

theorem singleton_inter_subset_left {α : Type} {X Y : Set α} {a : α} (ha : X ∩ Y = {a}) : {a} ⊆ X

theorem singleton_inter_subset_right {α : Type} {X Y : Set α} {a : α} (ha : X ∩ Y = {a}) : {a} ⊆ Y

theorem diff_subset_parent {α : Type} {X₁ X₂ E : Set α} (hX₁E : X₁ ⊆ E) : X₁ \ X₂ ⊆ E

Being a subset is preserved under subtracting sets.

theorem inter_subset_parent_left {α : Type} {X₁ X₂ E : Set α} (hX₁E : X₁ ⊆ E) : X₁ ∩ X₂ ⊆ E

Being a subset is preserved under taking intersections.

theorem inter_subset_parent_right {α : Type} {X₁ X₂ E : Set α} (hX₂E : X₂ ⊆ E) : X₁ ∩ X₂ ⊆ E

Being a subset is preserved under taking intersections.

theorem inter_subset_union {α : Type} {X₁ X₂ : Set α} : X₁ ∩ X₂ ⊆ X₁ ∪ X₂

Intersection of two sets is subset of their union.

theorem subset_diff_empty_eq {α : Type} {A B : Set α} (hAB : A ⊆ B) (hBA : B \ A = ∅) : A = B

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

theorem disjoint_of_singleton_inter_left_wo {α : Type} {X Y : Set α} {a : α} (hXY : X ∩ Y = {a}) : X \ {a} ⫗ Y

theorem disjoint_of_singleton_inter_right_wo {α : Type} {X Y : Set α} {a : α} (hXY : X ∩ Y = {a}) : X ⫗ Y \ {a}

theorem disjoint_of_singleton_inter_both_wo {α : Type} {X Y : Set α} {a : α} (hXY : X ∩ Y = {a}) : X \ {a} ⫗ Y \ {a}

theorem disjoint_of_singleton_inter_subset_left {α : Type} {X Y Z : Set α} {a : α} (hXY : X ∩ Y = {a}) (hZ : Z ⊆ X) (haZ : a ∉ Z) : Z ⫗ Y

theorem disjoint_of_singleton_inter_subset_right {α : Type} {X Y Z : Set α} {a : α} (hXY : X ∩ Y = {a}) (hZ : Z ⊆ Y) (haZ : a ∉ Z) : X ⫗ Z

theorem disjoint_nonempty_not_subset {α : Type} {A B : Set α} (hAB : A ⫗ B) (hA : A.Nonempty) : ¬A ⊆ B

theorem disjoint_nonempty_not_ssubset {α : Type} {A B : Set α} (hAB : A ⫗ B) (hA : A.Nonempty) : ¬A ⊂ B

theorem ssubset_union_disjoint_nonempty {α : Type} {X Y : Set α} (hXY : X ⫗ Y) (hY : Y.Nonempty) : X ⊂ X ∪ Y

theorem union_ssubset_union_iff {α : Type} {A B X : Set α} (hAX : A ⫗ X) (hBX : B ⫗ X) : A ∪ X ⊂ B ∪ X ↔ A ⊂ B

theorem union_subset_union_iff {α : Type} {A B X : Set α} (hAX : A ⫗ X) (hBX : B ⫗ X) : A ∪ X ⊆ B ∪ X ↔ A ⊆ B

theorem ssubset_disjoint_union_nonempty {α : Type} {X₁ X₂ : Set α} (hXX : X₁ ⫗ X₂) (hX₂ : X₂.Nonempty) : X₁ ⊂ X₁ ∪ X₂

theorem ssubset_disjoint_nonempty_union {α : Type} {X₁ X₂ : Set α} (hXX : X₁ ⫗ X₂) (hX₁ : X₁.Nonempty) : X₂ ⊂ X₁ ∪ X₂

theorem disjoint_inter_disjoint {α : Type} {A B : Set α} (C : Set α) (hAB : A ⫗ B) : C ⫗ A ∩ B

If two sets are disjoint, then any set is disjoint with their intersection

theorem diff_inter_disjoint_diff_inter {α : Type} (X₁ X₂ : Set α) : X₁ \ (X₁ ∩ X₂) ⫗ X₂ \ (X₁ ∩ X₂)

theorem symmDiff_eq_alt {α : Type} (X Y : Set α) : symmDiff X Y = (X ∪ Y) \ (X ∩ Y)

Symmetric difference of two sets is their union minus their intersection.

theorem symmDiff_disjoint_inter {α : Type} (X Y : Set α) : symmDiff X Y ⫗ X ∩ Y

Symmetric difference of two sets is disjoint with their intersection.

theorem symmDiff_empty_eq {α : Type} (X : Set α) : symmDiff X ∅ = X

theorem empty_symmDiff_eq {α : Type} (X : Set α) : symmDiff ∅ X = X

theorem symmDiff_subset_ground_right {α : Type} {X Y E : Set α} (hE : symmDiff X Y ⊆ E) (hX : X ⊆ E) : Y ⊆ E

theorem symmDiff_subset_ground_left {α : Type} {X Y E : Set α} (hE : symmDiff X Y ⊆ E) (hX : Y ⊆ E) : X ⊆ E