little golf

Author: staroperator

Mathlib/SetTheory/Cardinal/Pigeonhole.lean

@@ -144,54 +144,46 @@ theorem Uncountable.exists_uncountable_pairwise_inter_eq {α : Type u} {ι : Typ
   | zero =>
     exact ⟨s, subset_rfl, ∅, hs, fun i hi j hj hij => by grind⟩
   | succ n ih =>
-    by_cases h : ∀ a, Countable {i ∈ s | a ∈ f i}
-    · let g : Ordinal.{v} → ι := 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
-        have hg : g j = Classical.epsilon fun i => i ∈ s ∧ ∀ k (hk : k < j), f i ∩ f (g k) = ∅ := by
-          simp only [g]
-          rw [WellFoundedLT.fix_eq]
-        suffices {i ∈ s | ∀ k (hk : k < j), f i ∩ f (g k) = ∅}.Nonempty by
-          simp only [nonempty_def, mem_setOf_eq] at this
-          apply Classical.epsilon_spec at this
-          rw [← hg] at this
-          exact this
-        apply Uncountable.nonempty
-        rw [setOf_and, setOf_mem_eq, ← diff_compl, ← diff_self_inter]
-        apply hs.to_set.diff
-        simp_rw [compl_setOf, not_forall, setOf_exists, ← mem_Iio, inter_iUnion₂]
-        apply Countable.biUnion
-        · rwa [← le_aleph0_iff_set_countable, mk_Iio_ordinal, lift_le_aleph0, ← lt_succ_iff,
-            succ_aleph0, ← lt_ord, ord_aleph]
-        · intro a ha
-          simp_rw [Finset.eq_empty_iff_forall_notMem, Finset.mem_inter, not_and', not_forall,
-            ← SetLike.mem_coe, setOf_exists, not_not, inter_iUnion₂]
-          apply Countable.biUnion
-          · apply Finite.countable
-            simp
-          · intro 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
-        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''
-        simp only [← hjk, Finset.inter_self] at this
-        simpa [this] using hn _ (hg j hj).1
-      refine ⟨g '' Iio ω₁, by grind, ∅, .to_subtype (.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]
-      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'
-    · simp only [not_forall, not_countable_iff] at h
-      rcases h with ⟨a, ha⟩
+    by_cases h : ∃ a, Uncountable {i ∈ s | a ∈ f i}
+    · rcases h with ⟨a, ha⟩
       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 =>
+      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
+        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.to_set.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
+      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''
+      simp only [← hjk, Finset.inter_self] at this
+      simpa [this] using hn _ (hg j hj).1
+    refine ⟨g '' Iio ω₁, by grind, ∅, .to_subtype (.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]
+    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'