feat(Data/Set): add result that shows a set is even iff it splits into two sets of equal cardinality

Mathlib/Data/Finset/Card.lean

@@ -733,6 +733,12 @@ theorem card_eq_three : #s = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z 
     simp only [xy, xz, yz, mem_insert, card_insert_of_not_mem, not_false_iff, mem_singleton,
       or_self_iff, card_singleton]
 
+theorem exists_disjoint_union_of_even_card (he : Even #s) :
+    ∃ (t u : Finset α), t ∪ u = s ∧ Disjoint t u ∧ #t = #u :=
+  let ⟨n, hn⟩ := he
+  let ⟨t, ht, ht'⟩ := exists_subset_card_eq (show n ≤ #s by omega)
+  ⟨t, s \ t, by simp [card_sdiff, disjoint_sdiff, *]⟩
+
 end DecidableEq
 
 theorem two_lt_card_iff : 2 < #s ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c := by

Mathlib/Data/Set/Basic.lean

@@ -1259,6 +1259,14 @@ lemma disjoint_union_left : Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t
 @[simp]
 lemma disjoint_union_right : Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u := disjoint_sup_right
 
+@[simp]
+theorem disjoint_insert_left : Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t := by
+  simp only [Set.disjoint_left, Set.mem_insert_iff, forall_eq_or_imp]
+
+@[simp]
+theorem disjoint_insert_right : Disjoint s (insert a t) ↔ a ∉ s ∧ Disjoint s t :=
+  disjoint_comm.trans <| by rw [disjoint_insert_left, _root_.disjoint_comm]
+
 @[simp] lemma disjoint_empty (s : Set α) : Disjoint s ∅ := disjoint_bot_right
 @[simp] lemma empty_disjoint (s : Set α) : Disjoint ∅ s := disjoint_bot_left
 

Mathlib/Data/Set/Card.lean

@@ -3,6 +3,7 @@ Copyright (c) 2023 Peter Nelson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Peter Nelson
 -/
+import Mathlib.SetTheory.Cardinal.Arithmetic
 import Mathlib.SetTheory.Cardinal.Finite
 
 /-!
@@ -618,12 +619,12 @@ theorem ncard_exchange' {a b : α} (ha : a ∉ s) (hb : b ∈ s) :
   rw [← ncard_exchange ha hb, ← singleton_union, ← singleton_union, union_diff_distrib,
     @diff_singleton_eq_self _ b {a} fun h ↦ ha (by rwa [← mem_singleton_iff.mp h])]
 
-lemma odd_card_insert_iff {a : α} (hs : s.Finite := by toFinite_tac) (ha : a ∉ s) :
+lemma odd_card_insert_iff {a : α} (ha : a ∉ s) (hs : s.Finite := by toFinite_tac) :
     Odd (insert a s).ncard ↔ Even s.ncard := by
   rw [ncard_insert_of_not_mem ha hs, Nat.odd_add]
   simp only [Nat.odd_add, ← Nat.not_even_iff_odd, Nat.not_even_one, iff_false, Decidable.not_not]
 
-lemma even_card_insert_iff {a : α} (hs : s.Finite := by toFinite_tac) (ha : a ∉ s) :
+lemma even_card_insert_iff {a : α} (ha : a ∉ s) (hs : s.Finite := by toFinite_tac) :
     Even (insert a s).ncard ↔ Odd s.ncard := by
   rw [ncard_insert_of_not_mem ha hs, Nat.even_add_one, Nat.not_even_iff_odd]
 
@@ -1060,5 +1061,52 @@ theorem ncard_eq_three : s.ncard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y 
   · rwa [ENat.coe_toNat] at h; rintro h'; simp [h'] at h
   simp [h]
 
+theorem exists_union_disjoint_ncard_eq_of_even_finite [DecidableEq α] (he : Even s.ncard)
+    (hs : s.Finite := by toFinite_tac) : ∃ (t u : Set α),
+    t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard := by
+  rw [ncard_eq_toFinset_card s hs] at he
+  obtain ⟨t, u, hutu, hdtu, hctu⟩ := Finset.exists_disjoint_union_of_even_card he
+  use t.toSet, u.toSet
+  simp only [← Finset.coe_union, Finite.coe_toFinset, Finset.disjoint_coe, ncard_coe_Finset,
+    and_self, hutu, hdtu, hctu]
+
+open Cardinal
+
+theorem exists_union_disjoint_cardinal_eq_of_infinite (h : s.Infinite) : ∃ (t u : Set α),
+    t ∪ u = s ∧ Disjoint t u ∧ #t = #u := by
+  have := h.to_subtype
+  have f : s ≃ s ⊕ s := by
+    apply Classical.choice
+    rw [← Cardinal.eq, ← add_def, add_mk_eq_self]
+  refine ⟨Subtype.val '' (f ⁻¹' (range .inl)), Subtype.val '' (f ⁻¹' (range .inr)), ?_, ?_, ?_⟩
+  · rw [← image_union, ← preimage_union]
+    simp
+  · exact disjoint_image_of_injective Subtype.val_injective
+      (isCompl_range_inl_range_inr.disjoint.preimage f)
+  · simp [mk_image_eq Subtype.val_injective]
+
+theorem exists_union_disjoint_cardinal_eq_iff [DecidableEq α] (s : Set α) :
+    Even (s.ncard) ↔ ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #t = #u := by
+  constructor <;> intro h
+  · obtain hfin | hnfin := s.finite_or_infinite
+    · obtain ⟨t, u, rfl, htu2, htu3⟩ := exists_union_disjoint_ncard_eq_of_even_finite h hfin
+      use t, u
+      refine ⟨rfl, htu2, ?_⟩
+      simp only [← @card_coe_set_eq] at htu3
+      rw [finite_union] at hfin
+      exact Cardinal.toNat_injOn (mem_Iio.mpr (Finite.lt_aleph0 hfin.1))
+        (mem_Iio.mpr (Finite.lt_aleph0 hfin.2)) htu3
+    · exact exists_union_disjoint_cardinal_eq_of_infinite hnfin
+  · obtain ⟨t, u, rfl, htu2, htu3⟩ := h
+    obtain hfin | hnfin := (t ∪ u).finite_or_infinite
+    · rw [finite_union] at hfin
+      rw [ncard_union_eq htu2 hfin.1 hfin.2]
+      have hn : Cardinal.toNat (Cardinal.mk t) = Cardinal.toNat (Cardinal.mk u) := by
+        congr
+      simp only [← Nat.card.eq_1, Nat.card_coe_set_eq] at hn
+      rw [hn]
+      exact Even.add_self u.ncard
+    · simp only [hnfin.ncard, even_zero]
+
 end ncard
 end Set