generalize

Author: staroperator

Mathlib/SetTheory/Cardinal/Pigeonhole.lean

@@ -124,66 +124,85 @@ theorem le_range_of_union_finset_eq_univ {α β : Type*} [Infinite β] (f : α 
 @[deprecated (since := "2026-01-17")] alias le_range_of_union_finset_eq_top :=
   le_range_of_union_finset_eq_univ
 
-end Cardinal
-
-open Cardinal
-
-/-- **Δ-system lemma**: every uncountable family of finite sets must contain an uncountable
-Δ-system, i.e. an uncountable subfamily that share the same pairwise intersection. -/
-theorem Uncountable.exists_uncountable_pairwise_inter_eq {α : Type u} {ι : Type v} [DecidableEq α]
-    [Uncountable ι] (f : ι → Finset α) :
-    ∃ (s : Set ι) (t : Finset α), s.Uncountable ∧ s.Pairwise (f · ∩ f · = t) := by
-  suffices ∀ (s : Set ι) (n : ℕ), (∀ i ∈ s, (f i).card = n) → s.Uncountable →
-      ∃ s' ⊆ s, ∃ (t : Finset α), s'.Uncountable ∧ s'.Pairwise (f · ∩ f · = t) by
-    rcases exists_uncountable_fiber (fun i => ULift.up (f i).card) (by simp) (by infer_instance)
-      with ⟨⟨n⟩, h⟩
-    rcases this _ n (by grind) h.to_set with ⟨s', -, t, hs, ht⟩
-    exact ⟨s', t, hs, ht⟩
+/-- **Δ-system lemma**: let `κ` be an uncountable regular cardinal, every family of at least κ
+finite sets must contain a Δ-system with size κ, i.e. a subfamily that share the same pairwise
+intersection. -/
+theorem IsRegular.exists_pairwise_inter_eq_finset {α ι : Type u} [DecidableEq α]
+    (f : ι → Finset α) {κ : Cardinal} (hκ : ℵ₀ < κ) (hκ' : κ.IsRegular) (hι : κ ≤ #ι) :
+    ∃ (s : Set ι) (t : Finset α), #s = κ ∧ s.Pairwise (f · ∩ f · = t) := by
+  suffices ∀ (s : Set ι) (n : ℕ), (∀ i ∈ s, (f i).card = n) → κ ≤ #s →
+      ∃ s' ⊆ s, ∃ (t : Finset α), κ ≤ #s' ∧ s'.Pairwise (f · ∩ f · = t) by
+    rcases infinite_pigeonhole_card (fun i => ULift.up (f i).card) κ hι hκ.le
+      (by simpa [hκ'.cof_eq]) with ⟨⟨n⟩, h⟩
+    rcases this _ n (by grind) h with ⟨s, -, t, hs, ht⟩
+    rw [le_mk_iff_exists_subset] at hs
+    rcases hs with ⟨s', hs', hs''⟩
+    exact ⟨s', t, hs'', ht.mono hs'⟩
   intro s n hn hs
   induction n generalizing f s with
   | zero =>
     exact ⟨s, subset_rfl, ∅, hs, fun i hi j hj hij => by grind⟩
   | succ n ih =>
-    by_cases h : ∃ a, Uncountable {i ∈ s | a ∈ f i}
+    by_cases h : ∃ a, κ ≤ #{i ∈ s | a ∈ f i}
     · rcases h with ⟨a, ha⟩
-      rcases ih (fun i => f i \ {a}) _ (by grind) ha.to_set with ⟨s', hs', t, hs'', ht⟩
+      rcases ih (fun i => f i \ {a}) _ (by grind) ha with ⟨s', hs', t, hs'', ht⟩
       exact ⟨s', hs'.trans (sep_subset _ _), t ∪ {a}, hs'', fun i hi j hj hij => by
         grind [Set.Pairwise]⟩
-    simp only [coe_setOf, not_exists, not_uncountable_iff] at h
-    let g : Ordinal.{v} → ι := WellFoundedLT.fix fun j ih =>
+    simp only [not_exists, not_le] at h
+    haveI : Nonempty ι := by simpa [mk_ne_zero_iff] using (aleph0_pos.trans hκ |>.trans_le hι).ne'
+    let g : κ.ord.ToType → ι := WellFoundedLT.fix fun j ih =>
       Classical.epsilon fun i => i ∈ s ∧ ∀ k (hk : k < j), f i ∩ f (ih k hk) = ∅
-    have hg : ∀ j < ω₁, g j ∈ s ∧ ∀ k < j, f (g j) ∩ f (g k) = ∅ := by
-      intro j hj
-      suffices {i ∈ s | ∀ k (hk : k < j), f i ∩ f (g k) = ∅}.Nonempty by
-        simp only [nonempty_def, mem_setOf_eq] at this
+    have hg : ∀ j, g j ∈ s ∧ ∀ k < j, f (g j) ∩ f (g k) = ∅ := by
+      intro j
+      suffices ∃ i ∈ s, ∀ k (hk : k < j), f i ∩ f (g k) = ∅ by
         apply Classical.epsilon_spec at this
         unfold g
         rwa [WellFoundedLT.fix_eq]
-      rw [setOf_and, setOf_mem_eq, ← diff_compl, ← diff_self_inter]
-      refine (hs.diff ?_).nonempty
-      simp_rw [compl_setOf, not_forall, setOf_exists, ← mem_Iio, inter_iUnion₂]
-      refine .biUnion ?_ fun a ha => ?_
-      · rwa [← le_aleph0_iff_set_countable, mk_Iio_ordinal, lift_le_aleph0, ← lt_succ_iff,
-          succ_aleph0, ← lt_ord, ord_aleph]
-      · simp_rw [Finset.eq_empty_iff_forall_notMem, Finset.mem_inter, not_and', not_forall,
-          ← SetLike.mem_coe, setOf_exists, not_not, inter_iUnion₂]
-        refine .biUnion (Finset.finite_toSet _).countable fun i hi => ?_
-        simp_rw [SetLike.mem_coe, inter_setOf_eq_sep]
-        exact h i
-    have hg' : InjOn g (Iio ω₁) := by
-      intro j hj k hk hjk
+      suffices (s \ ⋃ k : Set.Iio j, ⋃ a : f (g k), {i ∈ s | a.1 ∈ f i}).Nonempty by
+        simp only [nonempty_def, mem_diff, mem_iUnion, mem_setOf_eq, Subtype.exists, not_exists]
+          at this
+        grind
+      apply Cardinal.diff_nonempty_of_mk_lt_mk
+      apply hs.trans_lt'
+      apply mk_iUnion_le_sum_mk.trans_lt
+      apply sum_lt_of_isRegular hκ' (mk_Iio_ord_toType _)
+      intro ⟨k, hk⟩
+      apply mk_iUnion_le_sum_mk.trans_lt
+      apply sum_lt_of_isRegular hκ' (hκ.trans_le' (by simp))
+      intro
+      apply h
+    have hg' : g.Injective := by
+      intro j k hjk
       by_contra hjk'
       wlog hjk'' : k < j generalizing j k
-      · exact this hk hj hjk.symm (ne_comm.1 hjk') (lt_of_le_of_ne (le_of_not_gt hjk'') hjk')
-      have := (hg j hj).2 k hjk''
+      · exact this hjk.symm (ne_comm.1 hjk') (lt_of_le_of_ne (le_of_not_gt hjk'') hjk')
+      have := (hg j).2 k hjk''
       simp only [← hjk, Finset.inter_self] at this
-      simpa [this] using hn _ (hg j hj).1
-    refine ⟨g '' Iio ω₁, by grind, ∅, .image ?_ hg', Pairwise.image ?_⟩
-    · rw [← uncountable_coe_iff, ← aleph0_lt_mk_iff, mk_Iio_ordinal, aleph0_lt_lift, card_omega]
-      exact aleph0_lt_aleph_one
-    intro j hj k hk hjk
-    simp only [Function.onFun_apply]
+      simpa [this] using hn _ (hg j).1
+    refine ⟨range g, by grind, ∅, by rw [mk_range_eq _ hg', mk_ord_toType],
+      Pairwise.range_pairwise ?_⟩
+    intro j k hjk
     wlog hjk' : k < j generalizing j k
-    · rw [Finset.inter_comm]
-      exact this hk hj hjk.symm (lt_of_le_of_ne (le_of_not_gt hjk') hjk)
-    exact (hg j hj).2 k hjk'
+    · rw [Function.onFun_apply, Finset.inter_comm]
+      exact this hjk.symm (lt_of_le_of_ne (le_of_not_gt hjk') hjk)
+    exact (hg j).2 k hjk'
+
+end Cardinal
+
+open Cardinal
+
+/-- **Δ-system lemma** for uncountable families, i.e. `κ = ℵ₁`. -/
+theorem Uncountable.exists_uncountable_pairwise_inter_eq_finset {α : Type u} {ι : Type v}
+    [DecidableEq α] [Uncountable ι] (f : ι → Finset α) :
+    ∃ (s : Set ι) (t : Finset α), s.Uncountable ∧ s.Pairwise (f · ∩ f · = t) := by
+  rcases isRegular_aleph_one.exists_pairwise_inter_eq_finset
+    (fun i : ULift.{u} ι => Equiv.ulift.symm.finsetCongr (f i.down))
+    aleph0_lt_aleph_one (by simp [← succ_aleph0]) with ⟨s, t, hs, ht⟩
+  refine ⟨Equiv.Set.congr Equiv.ulift s, Equiv.ulift.finsetCongr t, ?_, ?_⟩
+  · rw [← uncountable_coe_iff, ← aleph0_lt_mk_iff, Equiv.Set.congr_apply, ← Cardinal.lift_lt,
+      mk_image_eq_lift _ _ Equiv.ulift.injective, hs, lift_aleph0, lift_aleph, Ordinal.lift_one]
+    exact aleph0_lt_aleph_one
+  · apply Pairwise.image
+    simp_rw [← Equiv.ulift.finsetCongr.symm_apply_eq, Equiv.finsetCongr_symm,
+      Equiv.finsetCongr_apply, Finset.map_inter]
+    exact ht