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 := by
+  rw [disjoint_comm, disjoint_insert_left, 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,45 @@ 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]
 
+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)), ?_, ?_, ?_⟩
+  · simp [← image_union, ← preimage_union]
+  · 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_of_even (he : Even s.ncard) : ∃ (t u : Set α),
+    t ∪ u = s ∧ Disjoint t u ∧ #t = #u := by
+  obtain hs | hs := s.infinite_or_finite
+  · exact exists_union_disjoint_cardinal_eq_of_infinite hs
+  classical
+  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 [← Finset.coe_union, *]
+
+theorem exists_union_disjoint_ncard_eq_of_even (he : Even s.ncard) : ∃ (t u : Set α),
+    t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard := by
+  obtain ⟨t, u, hutu, hdtu, hctu⟩ := exists_union_disjoint_cardinal_eq_of_even he
+  exact ⟨t, u, hutu, hdtu, congrArg Cardinal.toNat hctu⟩
+
+theorem exists_union_disjoint_cardinal_eq_iff (s : Set α) :
+    Even (s.ncard) ↔ ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #t = #u := by
+  use exists_union_disjoint_cardinal_eq_of_even
+  rintro ⟨t, u, rfl, hdtu, hctu⟩
+  obtain hfin | hnfin := (t ∪ u).finite_or_infinite
+  · rw [finite_union] at hfin
+    have hn : t.ncard = u.ncard := congrArg Cardinal.toNat hctu
+    rw [ncard_union_eq hdtu hfin.1 hfin.2, hn]
+    exact Even.add_self u.ncard
+  · simp [hnfin.ncard]
+
 end ncard
 end Set