From 241095d3979db9142ea165f495a03e53b2b63cc9 Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Mon, 11 Nov 2024 16:26:40 +0100 Subject: [PATCH 01/11] feat(Data/Set): Even sets partition into two sets of the same cardinality --- Mathlib/Data/Set/Basic.lean | 8 +++ Mathlib/Data/Set/Card.lean | 133 +++++++++++++++++++++++++++++++++++- 2 files changed, 139 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index 4e529dbcb572b..7410fdc102e2d 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/Mathlib/Data/Set/Basic.lean @@ -1260,6 +1260,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 diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean index e4c5eaa625091..41eb4a1cbd2f3 100644 --- a/Mathlib/Data/Set/Card.lean +++ b/Mathlib/Data/Set/Card.lean @@ -3,8 +3,10 @@ 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 + /-! # Noncomputable Set Cardinality @@ -619,12 +621,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] @@ -1055,5 +1057,132 @@ 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_cardinal_eq_of_even_finite [DecidableEq α] (s : Set α) + (he : Even s.ncard) (hs : s.Finite := by toFinite_tac) : ∃ (t u : Set α), + t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard := by + obtain rfl | h := s.eq_empty_or_nonempty + · use ∅, ∅ + simp only [Set.union_self, disjoint_self, Set.bot_eq_empty, and_self] + · obtain ⟨x, y, hxy⟩ := (Set.one_lt_ncard_iff hs).mp (one_lt_ncard_of_nonempty_of_even hs h he) + have hsi : insert x (insert y (s \ {x, y})) = s := by + ext v + simp only [mem_insert_iff, mem_diff, mem_singleton_iff, not_or] + constructor <;> intro h + · cases' h with hl hr + · rw [hl]; exact hxy.1 + · cases' hr with h1 h2 + · rw [h1]; exact hxy.2.1 + · exact h2.1 + · by_cases hc : v = x ∨ v = y + · rw [← or_assoc] + left + exact hc + · right; right + push_neg at hc + exact ⟨h, hc⟩ + have hu'e : Even ((s \ {x, y}).ncard):= by + rw [← odd_card_insert_iff (by + simp only [mem_diff, mem_insert_iff, mem_singleton_iff, or_true, not_true_eq_false, + and_false, not_false_eq_true] : y ∉ s \ {x, y}) (hs.diff _)] + rw [← even_card_insert_iff (by simp only [mem_insert_iff, hxy.2.2, + mem_diff, mem_singleton_iff, or_false, not_true_eq_false, and_false, or_self, + not_false_eq_true] : x ∉ insert y (s \ {x, y}) ) ((hs.diff _).insert _)] + rw [hsi] + exact he + obtain ⟨t, u, hst⟩ := exists_union_disjoint_cardinal_eq_of_even_finite _ hu'e (hs.diff _) + use insert x t, insert y u + refine ⟨by simp only [union_insert, insert_union, hst.1, insert_comm, hsi], ?_⟩ + have hynt : y ∉ t := fun hys ↦ by simpa [hst.1] using (Set.subset_union_left hys : y ∈ t ∪ u) + have hxnu : x ∉ u := fun hxt ↦ by simpa [hst.1] using (Set.subset_union_right hxt : x ∈ t ∪ u) + have hynu : y ∉ u := fun hys ↦ by simpa [hst.1] using (Set.subset_union_right hys : y ∈ t ∪ u) + have hxnt : x ∉ t := fun hxs ↦ by simpa [hst.1] using (Set.subset_union_left hxs : x ∈ t ∪ u) + have htuf : (t ∪ u).Finite := by + rw [hst.1] + exact Finite.diff hs {x, y} + constructor <;> simp [hxnu, hynt, hst.2.1, hxy.2.2.symm, + Set.ncard_insert_of_not_mem hxnt (Set.finite_union.mp htuf).1, + Set.ncard_insert_of_not_mem hynu (Set.finite_union.mp htuf).2, hst.2.2] +termination_by s.ncard +decreasing_by +· simp_wf + refine Set.ncard_lt_ncard ?_ hs + exact ⟨Set.diff_subset, by + rw [Set.not_subset_iff_exists_mem_not_mem] + use x + exact ⟨hxy.1, by simp only [Set.mem_diff, Set.mem_insert_iff, Set.mem_singleton_iff, true_or, + not_true_eq_false, and_false, not_false_eq_true]⟩⟩ + +theorem exists_union_disjoint_cardinal_eq_of_infinite [DecidableEq α] (s : Set α) + (h : s.Infinite) : ∃ (t u : Set α), + t ∪ u = s ∧ Disjoint t u ∧ Cardinal.mk t = Cardinal.mk u := by + have f : s ⊕ s ≃ s := by + have : Inhabited (s ⊕ s ≃ s) := by + apply Classical.inhabited_of_nonempty + rw [← Cardinal.eq, Cardinal.mk_sum, Cardinal.add_eq_max (by + rw [@Cardinal.aleph0_le_lift] + exact Cardinal.infinite_iff.mp (Set.infinite_coe_iff.mpr h) + )] + simp only [Cardinal.lift_id, max_self] + exact this.default + use Subtype.val '' (f '' (Sum.inl '' Set.univ)), Subtype.val '' (f '' (Sum.inr '' Set.univ)) + constructor + · ext v + simp only [Set.image_univ, Set.mem_union, Set.mem_image, Set.mem_image_equiv, Set.mem_range, + Subtype.exists, exists_and_right, exists_eq_right] + refine ⟨fun h ↦ by + cases' h with hl hr + · obtain ⟨hvu, _⟩ := hl + exact hvu + · obtain ⟨hvu, _⟩ := hr + exact hvu, ?_⟩ + · intro hv + rw [← exists_or] + use hv + simp only [Sum.exists, Sum.inl.injEq, exists_subtype_mk_eq_iff, exists_eq, true_and, + Subtype.exists, reduceCtorEq, exists_false, false_and, or_false, Sum.inr.injEq, false_or] + obtain ⟨a, ha⟩ := f.surjective ⟨v, hv⟩ + rw [← ha] + simp only [EmbeddingLike.apply_eq_iff_eq] + cases' a with l r + · left; use l, l.coe_prop + · right; use r, r.coe_prop + · constructor + · simp only [Set.image_univ, ← Set.image_comp] + apply Set.disjoint_image_of_injective (by + simp only [Subtype.val_injective, Function.Injective.of_comp_iff, f.injective]) + rw [Set.disjoint_right] + intro a ha + simp only [Set.mem_range, Subtype.exists, not_exists] at * + intro v hv + obtain ⟨_, _, h⟩ := ha + rw [← h] + exact Sum.inl_ne_inr + · simp only [Set.image_univ, Subtype.val_injective, Cardinal.mk_image_eq, f.injective, + Sum.inl_injective, Cardinal.mk_range_eq, Sum.inr_injective] + + +theorem exists_union_disjoint_cardinal_eq_iff [DecidableEq α] (s : Set α) : + Even (s.ncard) ↔ ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ Cardinal.mk t = Cardinal.mk u := by + constructor <;> intro h + · obtain hfin | hnfin := s.finite_or_infinite + · obtain ⟨t, u, rfl, htu2, htu3⟩ := exists_union_disjoint_cardinal_eq_of_even_finite _ h hfin + use t, u + refine ⟨rfl, htu2, ?_⟩ + simp only [← @card_coe_set_eq, Nat.card.eq_1] at htu3 + rw [Set.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 s hnfin + · obtain ⟨t, u, rfl, htu2, htu3⟩ := h + obtain hfin | hnfin := (t ∪ u).finite_or_infinite + · rw [Set.finite_union] at hfin + rw [Set.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, Set.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 From f54e8138eac5ff213b248e662d94f3d57b9430ae Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Mon, 11 Nov 2024 16:28:38 +0100 Subject: [PATCH 02/11] Cleanup --- Mathlib/Data/Set/Card.lean | 48 +++++++++++++++++++------------------- 1 file changed, 24 insertions(+), 24 deletions(-) diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean index 41eb4a1cbd2f3..e3191fe78ce3b 100644 --- a/Mathlib/Data/Set/Card.lean +++ b/Mathlib/Data/Set/Card.lean @@ -1062,8 +1062,8 @@ theorem exists_union_disjoint_cardinal_eq_of_even_finite [DecidableEq α] (s : S t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard := by obtain rfl | h := s.eq_empty_or_nonempty · use ∅, ∅ - simp only [Set.union_self, disjoint_self, Set.bot_eq_empty, and_self] - · obtain ⟨x, y, hxy⟩ := (Set.one_lt_ncard_iff hs).mp (one_lt_ncard_of_nonempty_of_even hs h he) + simp only [union_self, disjoint_self, bot_eq_empty, and_self] + · obtain ⟨x, y, hxy⟩ := (one_lt_ncard_iff hs).mp (one_lt_ncard_of_nonempty_of_even hs h he) have hsi : insert x (insert y (s \ {x, y})) = s := by ext v simp only [mem_insert_iff, mem_diff, mem_singleton_iff, not_or] @@ -1092,24 +1092,24 @@ theorem exists_union_disjoint_cardinal_eq_of_even_finite [DecidableEq α] (s : S obtain ⟨t, u, hst⟩ := exists_union_disjoint_cardinal_eq_of_even_finite _ hu'e (hs.diff _) use insert x t, insert y u refine ⟨by simp only [union_insert, insert_union, hst.1, insert_comm, hsi], ?_⟩ - have hynt : y ∉ t := fun hys ↦ by simpa [hst.1] using (Set.subset_union_left hys : y ∈ t ∪ u) - have hxnu : x ∉ u := fun hxt ↦ by simpa [hst.1] using (Set.subset_union_right hxt : x ∈ t ∪ u) - have hynu : y ∉ u := fun hys ↦ by simpa [hst.1] using (Set.subset_union_right hys : y ∈ t ∪ u) - have hxnt : x ∉ t := fun hxs ↦ by simpa [hst.1] using (Set.subset_union_left hxs : x ∈ t ∪ u) + have hynt : y ∉ t := fun hys ↦ by simpa [hst.1] using (subset_union_left hys : y ∈ t ∪ u) + have hxnu : x ∉ u := fun hxt ↦ by simpa [hst.1] using (subset_union_right hxt : x ∈ t ∪ u) + have hynu : y ∉ u := fun hys ↦ by simpa [hst.1] using (subset_union_right hys : y ∈ t ∪ u) + have hxnt : x ∉ t := fun hxs ↦ by simpa [hst.1] using (subset_union_left hxs : x ∈ t ∪ u) have htuf : (t ∪ u).Finite := by rw [hst.1] exact Finite.diff hs {x, y} constructor <;> simp [hxnu, hynt, hst.2.1, hxy.2.2.symm, - Set.ncard_insert_of_not_mem hxnt (Set.finite_union.mp htuf).1, - Set.ncard_insert_of_not_mem hynu (Set.finite_union.mp htuf).2, hst.2.2] + ncard_insert_of_not_mem hxnt (finite_union.mp htuf).1, + ncard_insert_of_not_mem hynu (finite_union.mp htuf).2, hst.2.2] termination_by s.ncard decreasing_by · simp_wf - refine Set.ncard_lt_ncard ?_ hs - exact ⟨Set.diff_subset, by - rw [Set.not_subset_iff_exists_mem_not_mem] + refine ncard_lt_ncard ?_ hs + exact ⟨diff_subset, by + rw [not_subset_iff_exists_mem_not_mem] use x - exact ⟨hxy.1, by simp only [Set.mem_diff, Set.mem_insert_iff, Set.mem_singleton_iff, true_or, + exact ⟨hxy.1, by simp only [mem_diff, mem_insert_iff, mem_singleton_iff, true_or, not_true_eq_false, and_false, not_false_eq_true]⟩⟩ theorem exists_union_disjoint_cardinal_eq_of_infinite [DecidableEq α] (s : Set α) @@ -1120,14 +1120,14 @@ theorem exists_union_disjoint_cardinal_eq_of_infinite [DecidableEq α] (s : Set apply Classical.inhabited_of_nonempty rw [← Cardinal.eq, Cardinal.mk_sum, Cardinal.add_eq_max (by rw [@Cardinal.aleph0_le_lift] - exact Cardinal.infinite_iff.mp (Set.infinite_coe_iff.mpr h) + exact Cardinal.infinite_iff.mp (infinite_coe_iff.mpr h) )] simp only [Cardinal.lift_id, max_self] exact this.default - use Subtype.val '' (f '' (Sum.inl '' Set.univ)), Subtype.val '' (f '' (Sum.inr '' Set.univ)) + use Subtype.val '' (f '' (Sum.inl '' univ)), Subtype.val '' (f '' (Sum.inr '' univ)) constructor · ext v - simp only [Set.image_univ, Set.mem_union, Set.mem_image, Set.mem_image_equiv, Set.mem_range, + simp only [image_univ, mem_union, mem_image, mem_image_equiv, mem_range, Subtype.exists, exists_and_right, exists_eq_right] refine ⟨fun h ↦ by cases' h with hl hr @@ -1147,17 +1147,17 @@ theorem exists_union_disjoint_cardinal_eq_of_infinite [DecidableEq α] (s : Set · left; use l, l.coe_prop · right; use r, r.coe_prop · constructor - · simp only [Set.image_univ, ← Set.image_comp] - apply Set.disjoint_image_of_injective (by + · simp only [image_univ, ← image_comp] + apply disjoint_image_of_injective (by simp only [Subtype.val_injective, Function.Injective.of_comp_iff, f.injective]) - rw [Set.disjoint_right] + rw [disjoint_right] intro a ha - simp only [Set.mem_range, Subtype.exists, not_exists] at * + simp only [mem_range, Subtype.exists, not_exists] at * intro v hv obtain ⟨_, _, h⟩ := ha rw [← h] exact Sum.inl_ne_inr - · simp only [Set.image_univ, Subtype.val_injective, Cardinal.mk_image_eq, f.injective, + · simp only [image_univ, Subtype.val_injective, Cardinal.mk_image_eq, f.injective, Sum.inl_injective, Cardinal.mk_range_eq, Sum.inr_injective] @@ -1169,17 +1169,17 @@ theorem exists_union_disjoint_cardinal_eq_iff [DecidableEq α] (s : Set α) : use t, u refine ⟨rfl, htu2, ?_⟩ simp only [← @card_coe_set_eq, Nat.card.eq_1] at htu3 - rw [Set.finite_union] at hfin + 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 s hnfin · obtain ⟨t, u, rfl, htu2, htu3⟩ := h obtain hfin | hnfin := (t ∪ u).finite_or_infinite - · rw [Set.finite_union] at hfin - rw [Set.ncard_union_eq htu2 hfin.1 hfin.2] + · 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, Set.Nat.card_coe_set_eq] at hn + 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] From b4a662fddf28cc9227290be7d42f38a5618660c4 Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Mon, 11 Nov 2024 16:34:09 +0100 Subject: [PATCH 03/11] Remove extra newline --- Mathlib/Data/Set/Card.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean index e3191fe78ce3b..7194668b2cbb2 100644 --- a/Mathlib/Data/Set/Card.lean +++ b/Mathlib/Data/Set/Card.lean @@ -6,7 +6,6 @@ Authors: Peter Nelson import Mathlib.SetTheory.Cardinal.Arithmetic import Mathlib.SetTheory.Cardinal.Finite - /-! # Noncomputable Set Cardinality From 213d00d091fb57819a3306716960d169aff2ee70 Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Mon, 11 Nov 2024 16:38:23 +0100 Subject: [PATCH 04/11] Whitespace fixes --- Mathlib/Data/Set/Basic.lean | 2 +- Mathlib/Data/Set/Card.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index 7410fdc102e2d..45fca0d243ccd 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/Mathlib/Data/Set/Basic.lean @@ -1267,7 +1267,7 @@ theorem disjoint_insert_left : Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint @[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 diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean index 7194668b2cbb2..342d99afcea15 100644 --- a/Mathlib/Data/Set/Card.lean +++ b/Mathlib/Data/Set/Card.lean @@ -1057,7 +1057,7 @@ theorem ncard_eq_three : s.ncard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y simp [h] theorem exists_union_disjoint_cardinal_eq_of_even_finite [DecidableEq α] (s : Set α) - (he : Even s.ncard) (hs : s.Finite := by toFinite_tac) : ∃ (t u : Set α), + (he : Even s.ncard) (hs : s.Finite := by toFinite_tac) : ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard := by obtain rfl | h := s.eq_empty_or_nonempty · use ∅, ∅ @@ -1112,7 +1112,7 @@ decreasing_by not_true_eq_false, and_false, not_false_eq_true]⟩⟩ theorem exists_union_disjoint_cardinal_eq_of_infinite [DecidableEq α] (s : Set α) - (h : s.Infinite) : ∃ (t u : Set α), + (h : s.Infinite) : ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ Cardinal.mk t = Cardinal.mk u := by have f : s ⊕ s ≃ s := by have : Inhabited (s ⊕ s ≃ s) := by From 1f30fa002b5438fc0b0c6d05b5502496792f7624 Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Tue, 12 Nov 2024 08:39:01 +0100 Subject: [PATCH 05/11] PR review comments and polishing --- Mathlib/Data/Finset/Card.lean | 6 +++ Mathlib/Data/Set/Card.lean | 71 ++++++----------------------------- 2 files changed, 17 insertions(+), 60 deletions(-) diff --git a/Mathlib/Data/Finset/Card.lean b/Mathlib/Data/Finset/Card.lean index b08d5c973026f..9c21317eb6dd6 100644 --- a/Mathlib/Data/Finset/Card.lean +++ b/Mathlib/Data/Finset/Card.lean @@ -735,6 +735,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 diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean index 342d99afcea15..e1a8f71e1f180 100644 --- a/Mathlib/Data/Set/Card.lean +++ b/Mathlib/Data/Set/Card.lean @@ -1056,69 +1056,20 @@ 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_cardinal_eq_of_even_finite [DecidableEq α] (s : Set α) - (he : Even s.ncard) (hs : s.Finite := by toFinite_tac) : ∃ (t u : Set α), - t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard := by - obtain rfl | h := s.eq_empty_or_nonempty - · use ∅, ∅ - simp only [union_self, disjoint_self, bot_eq_empty, and_self] - · obtain ⟨x, y, hxy⟩ := (one_lt_ncard_iff hs).mp (one_lt_ncard_of_nonempty_of_even hs h he) - have hsi : insert x (insert y (s \ {x, y})) = s := by - ext v - simp only [mem_insert_iff, mem_diff, mem_singleton_iff, not_or] - constructor <;> intro h - · cases' h with hl hr - · rw [hl]; exact hxy.1 - · cases' hr with h1 h2 - · rw [h1]; exact hxy.2.1 - · exact h2.1 - · by_cases hc : v = x ∨ v = y - · rw [← or_assoc] - left - exact hc - · right; right - push_neg at hc - exact ⟨h, hc⟩ - have hu'e : Even ((s \ {x, y}).ncard):= by - rw [← odd_card_insert_iff (by - simp only [mem_diff, mem_insert_iff, mem_singleton_iff, or_true, not_true_eq_false, - and_false, not_false_eq_true] : y ∉ s \ {x, y}) (hs.diff _)] - rw [← even_card_insert_iff (by simp only [mem_insert_iff, hxy.2.2, - mem_diff, mem_singleton_iff, or_false, not_true_eq_false, and_false, or_self, - not_false_eq_true] : x ∉ insert y (s \ {x, y}) ) ((hs.diff _).insert _)] - rw [hsi] - exact he - obtain ⟨t, u, hst⟩ := exists_union_disjoint_cardinal_eq_of_even_finite _ hu'e (hs.diff _) - use insert x t, insert y u - refine ⟨by simp only [union_insert, insert_union, hst.1, insert_comm, hsi], ?_⟩ - have hynt : y ∉ t := fun hys ↦ by simpa [hst.1] using (subset_union_left hys : y ∈ t ∪ u) - have hxnu : x ∉ u := fun hxt ↦ by simpa [hst.1] using (subset_union_right hxt : x ∈ t ∪ u) - have hynu : y ∉ u := fun hys ↦ by simpa [hst.1] using (subset_union_right hys : y ∈ t ∪ u) - have hxnt : x ∉ t := fun hxs ↦ by simpa [hst.1] using (subset_union_left hxs : x ∈ t ∪ u) - have htuf : (t ∪ u).Finite := by - rw [hst.1] - exact Finite.diff hs {x, y} - constructor <;> simp [hxnu, hynt, hst.2.1, hxy.2.2.symm, - ncard_insert_of_not_mem hxnt (finite_union.mp htuf).1, - ncard_insert_of_not_mem hynu (finite_union.mp htuf).2, hst.2.2] -termination_by s.ncard -decreasing_by -· simp_wf - refine ncard_lt_ncard ?_ hs - exact ⟨diff_subset, by - rw [not_subset_iff_exists_mem_not_mem] - use x - exact ⟨hxy.1, by simp only [mem_diff, mem_insert_iff, mem_singleton_iff, true_or, - not_true_eq_false, and_false, not_false_eq_true]⟩⟩ - -theorem exists_union_disjoint_cardinal_eq_of_infinite [DecidableEq α] (s : Set α) - (h : s.Infinite) : ∃ (t u : Set α), +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 := + let ⟨n, hn⟩ := he + let ⟨t, ht, ht'⟩ := exists_subset_card_eq (show n ≤ s.ncard by omega) + ⟨t, s \ t, by simp [disjoint_sdiff_self_right, Set.ncard_diff, *]⟩ + +theorem exists_union_disjoint_cardinal_eq_of_infinite (h : s.Infinite) : ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ Cardinal.mk t = Cardinal.mk u := by have f : s ⊕ s ≃ s := by have : Inhabited (s ⊕ s ≃ s) := by apply Classical.inhabited_of_nonempty rw [← Cardinal.eq, Cardinal.mk_sum, Cardinal.add_eq_max (by - rw [@Cardinal.aleph0_le_lift] + rw [Cardinal.aleph0_le_lift] exact Cardinal.infinite_iff.mp (infinite_coe_iff.mpr h) )] simp only [Cardinal.lift_id, max_self] @@ -1164,14 +1115,14 @@ theorem exists_union_disjoint_cardinal_eq_iff [DecidableEq α] (s : Set α) : Even (s.ncard) ↔ ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ Cardinal.mk t = Cardinal.mk u := by constructor <;> intro h · obtain hfin | hnfin := s.finite_or_infinite - · obtain ⟨t, u, rfl, htu2, htu3⟩ := exists_union_disjoint_cardinal_eq_of_even_finite _ h hfin + · 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, Nat.card.eq_1] 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 s hnfin + · 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 From c6168d2fceba0c147da28936ce15bcea8c09a6d1 Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Tue, 12 Nov 2024 08:42:39 +0100 Subject: [PATCH 06/11] Switch to derived proof --- Mathlib/Data/Set/Card.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean index e1a8f71e1f180..749df785e7c6c 100644 --- a/Mathlib/Data/Set/Card.lean +++ b/Mathlib/Data/Set/Card.lean @@ -1058,10 +1058,12 @@ theorem ncard_eq_three : s.ncard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y 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 := - let ⟨n, hn⟩ := he - let ⟨t, ht, ht'⟩ := exists_subset_card_eq (show n ≤ s.ncard by omega) - ⟨t, s \ t, by simp [disjoint_sdiff_self_right, Set.ncard_diff, *]⟩ + 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] theorem exists_union_disjoint_cardinal_eq_of_infinite (h : s.Infinite) : ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ Cardinal.mk t = Cardinal.mk u := by From 73c744dd2d84e2acd00e3c89c9cbfe03b8bb25b0 Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Tue, 12 Nov 2024 08:45:10 +0100 Subject: [PATCH 07/11] Remove extra newline --- Mathlib/Data/Set/Card.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean index 749df785e7c6c..52eefa17dbdb7 100644 --- a/Mathlib/Data/Set/Card.lean +++ b/Mathlib/Data/Set/Card.lean @@ -1112,7 +1112,6 @@ theorem exists_union_disjoint_cardinal_eq_of_infinite (h : s.Infinite) : ∃ (t · simp only [image_univ, Subtype.val_injective, Cardinal.mk_image_eq, f.injective, Sum.inl_injective, Cardinal.mk_range_eq, Sum.inr_injective] - theorem exists_union_disjoint_cardinal_eq_iff [DecidableEq α] (s : Set α) : Even (s.ncard) ↔ ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ Cardinal.mk t = Cardinal.mk u := by constructor <;> intro h From db494aa84e9f6899ea67ada9e6cf6fab2458306c Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Sun, 5 Jan 2025 07:47:52 +0100 Subject: [PATCH 08/11] Update Mathlib/Data/Set/Card.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Violeta Hernández --- Mathlib/Data/Set/Card.lean | 56 ++++++++------------------------------ 1 file changed, 11 insertions(+), 45 deletions(-) diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean index 52eefa17dbdb7..efb06bf63f5b5 100644 --- a/Mathlib/Data/Set/Card.lean +++ b/Mathlib/Data/Set/Card.lean @@ -1066,51 +1066,17 @@ theorem exists_union_disjoint_ncard_eq_of_even_finite [DecidableEq α] (he : Eve and_self, hutu, hdtu, hctu] theorem exists_union_disjoint_cardinal_eq_of_infinite (h : s.Infinite) : ∃ (t u : Set α), - t ∪ u = s ∧ Disjoint t u ∧ Cardinal.mk t = Cardinal.mk u := by - have f : s ⊕ s ≃ s := by - have : Inhabited (s ⊕ s ≃ s) := by - apply Classical.inhabited_of_nonempty - rw [← Cardinal.eq, Cardinal.mk_sum, Cardinal.add_eq_max (by - rw [Cardinal.aleph0_le_lift] - exact Cardinal.infinite_iff.mp (infinite_coe_iff.mpr h) - )] - simp only [Cardinal.lift_id, max_self] - exact this.default - use Subtype.val '' (f '' (Sum.inl '' univ)), Subtype.val '' (f '' (Sum.inr '' univ)) - constructor - · ext v - simp only [image_univ, mem_union, mem_image, mem_image_equiv, mem_range, - Subtype.exists, exists_and_right, exists_eq_right] - refine ⟨fun h ↦ by - cases' h with hl hr - · obtain ⟨hvu, _⟩ := hl - exact hvu - · obtain ⟨hvu, _⟩ := hr - exact hvu, ?_⟩ - · intro hv - rw [← exists_or] - use hv - simp only [Sum.exists, Sum.inl.injEq, exists_subtype_mk_eq_iff, exists_eq, true_and, - Subtype.exists, reduceCtorEq, exists_false, false_and, or_false, Sum.inr.injEq, false_or] - obtain ⟨a, ha⟩ := f.surjective ⟨v, hv⟩ - rw [← ha] - simp only [EmbeddingLike.apply_eq_iff_eq] - cases' a with l r - · left; use l, l.coe_prop - · right; use r, r.coe_prop - · constructor - · simp only [image_univ, ← image_comp] - apply disjoint_image_of_injective (by - simp only [Subtype.val_injective, Function.Injective.of_comp_iff, f.injective]) - rw [disjoint_right] - intro a ha - simp only [mem_range, Subtype.exists, not_exists] at * - intro v hv - obtain ⟨_, _, h⟩ := ha - rw [← h] - exact Sum.inl_ne_inr - · simp only [image_univ, Subtype.val_injective, Cardinal.mk_image_eq, f.injective, - Sum.inl_injective, Cardinal.mk_range_eq, Sum.inr_injective] + 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 ∧ Cardinal.mk t = Cardinal.mk u := by From 8570cbfb2d133c6f56740c493627651b052e80d7 Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Sun, 5 Jan 2025 08:03:43 +0100 Subject: [PATCH 09/11] Post review fixes --- Mathlib/Data/Set/Card.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean index bd5bd58d26d76..358cfb5d1bca5 100644 --- a/Mathlib/Data/Set/Card.lean +++ b/Mathlib/Data/Set/Card.lean @@ -1070,6 +1070,8 @@ theorem exists_union_disjoint_ncard_eq_of_even_finite [DecidableEq α] (he : Eve 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 @@ -1084,13 +1086,13 @@ theorem exists_union_disjoint_cardinal_eq_of_infinite (h : s.Infinite) : ∃ (t · 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 ∧ Cardinal.mk t = Cardinal.mk u := by + 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, Nat.card.eq_1] at htu3 + 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 @@ -1103,7 +1105,7 @@ theorem exists_union_disjoint_cardinal_eq_iff [DecidableEq α] (s : Set α) : congr simp only [← Nat.card.eq_1, Nat.card_coe_set_eq] at hn rw [hn] - exact even_add_self u.ncard + exact Even.add_self u.ncard · simp only [hnfin.ncard, even_zero] end ncard From dc11df1485a2a8040a218a3fac0797898ec515e3 Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Mon, 6 Jan 2025 13:15:09 +0100 Subject: [PATCH 10/11] Update Mathlib/Data/Set/Basic.lean Co-authored-by: Thomas Browning --- Mathlib/Data/Set/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index 9bce8c409fdef..889fa0b8045e1 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/Mathlib/Data/Set/Basic.lean @@ -1264,8 +1264,8 @@ theorem disjoint_insert_left : Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint 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] +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 From a9e39caab37a386890e7c439ed88dd7bb6cc35b1 Mon Sep 17 00:00:00 2001 From: Pim Otte Date: Mon, 6 Jan 2025 13:16:47 +0100 Subject: [PATCH 11/11] Adopted review suggestions --- Mathlib/Data/Set/Card.lean | 57 +++++++++++++++++--------------------- 1 file changed, 25 insertions(+), 32 deletions(-) diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean index 358cfb5d1bca5..558634196ed15 100644 --- a/Mathlib/Data/Set/Card.lean +++ b/Mathlib/Data/Set/Card.lean @@ -1061,15 +1061,6 @@ 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 α), @@ -1079,34 +1070,36 @@ theorem exists_union_disjoint_cardinal_eq_of_infinite (h : s.Infinite) : ∃ (t 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 + · 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_iff [DecidableEq α] (s : Set α) : +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 - 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] + 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