feat: basic set lemmas (#6010)

Mathlib/Analysis/BoundedVariation.lean

@@ -555,17 +555,6 @@ theorem comp_eq_of_monotoneOn (f : α → E) {t : Set β} (φ : β → α) (hφ
   exact comp_le_of_monotoneOn _ ψ hψ ψts
 #align evariation_on.comp_eq_of_monotone_on eVariationOn.comp_eq_of_monotoneOn
 
--- porting note: move to file `data.set.intervals.basic` once the port is over,
--- and use it in theorem `polynomialFunctions_closure_eq_top`
--- in the file `topology/continuous_function/weierstrass.lean`
-theorem _root_.Set.subsingleton_Icc_of_ge {α : Type _} [PartialOrder α] {a b : α} (h : b ≤ a) :
-    Set.Subsingleton (Icc a b) := by
-  rintro c ⟨ac, cb⟩ d ⟨ad, db⟩
-  cases le_antisymm (cb.trans h) ac
-  cases le_antisymm (db.trans h) ad
-  rfl
-#align set.subsingleton_Icc_of_ge Set.subsingleton_Icc_of_ge
-
 theorem comp_inter_Icc_eq_of_monotoneOn (f : α → E) {t : Set β} (φ : β → α) (hφ : MonotoneOn φ t)
     {x y : β} (hx : x ∈ t) (hy : y ∈ t) :
     eVariationOn (f ∘ φ) (t ∩ Icc x y) = eVariationOn f (φ '' t ∩ Icc (φ x) (φ y)) := by

Mathlib/Data/Set/Intervals/Basic.lean

@@ -767,6 +767,18 @@ theorem Icc_eq_singleton_iff : Icc a b = {c} ↔ a = c ∧ b = c := by
     exact Icc_self _
 #align set.Icc_eq_singleton_iff Set.Icc_eq_singleton_iff
 
+lemma subsingleton_Icc_of_ge (hba : b ≤ a) : Set.Subsingleton (Icc a b) :=
+  fun _x ⟨hax, hxb⟩ _y ⟨hay, hyb⟩ ↦ le_antisymm
+    (le_implies_le_of_le_of_le hxb hay hba) (le_implies_le_of_le_of_le hyb hax hba)
+#align set.subsingleton_Icc_of_ge Set.subsingleton_Icc_of_ge
+
+@[simp] lemma subsingleton_Icc_iff {α : Type _} [LinearOrder α] {a b : α} :
+    Set.Subsingleton (Icc a b) ↔ b ≤ a := by
+  refine' ⟨fun h ↦ _, subsingleton_Icc_of_ge⟩
+  contrapose! h
+  simp only [ge_iff_le, gt_iff_lt, not_subsingleton_iff]
+  exact ⟨a, ⟨le_refl _, h.le⟩, b, ⟨h.le, le_refl _⟩, h.ne⟩
+
 @[simp]
 theorem Icc_diff_left : Icc a b \ {a} = Ioc a b :=
   ext fun x => by simp [lt_iff_le_and_ne, eq_comm, and_right_comm]

Mathlib/Data/Set/Pairwise/Basic.lean

@@ -408,8 +408,41 @@ theorem pairwiseDisjoint_image_left_iff {f : α → β → γ} {s : Set α} {t :
     exact h (congr_arg Prod.snd <| ht (mk_mem_prod ha hx) (mk_mem_prod hb hy) hab)
 #align set.pairwise_disjoint_image_left_iff Set.pairwiseDisjoint_image_left_iff
 
+lemma exists_ne_mem_inter_of_not_pairwiseDisjoint
+    {f : ι → Set α} (h : ¬ s.PairwiseDisjoint f) :
+    ∃ i ∈ s, ∃ j ∈ s, ∃ (_hij : i ≠ j) (x : α), x ∈ f i ∩ f j := by
+  change ¬ ∀ i, i ∈ s → ∀ j, j ∈ s → i ≠ j → ∀ t, t ≤ f i → t ≤ f j → t ≤ ⊥ at h
+  simp only [not_forall] at h
+  obtain ⟨i, hi, j, hj, h_ne, t, hfi, hfj, ht⟩ := h
+  replace ht : t.Nonempty := by
+    rwa [le_bot_iff, bot_eq_empty, ← Ne.def, ← nonempty_iff_ne_empty] at ht
+  obtain ⟨x, hx⟩ := ht
+  exact ⟨i, hi, j, hj, h_ne, x, hfi hx, hfj hx⟩
+
+lemma exists_lt_mem_inter_of_not_pairwiseDisjoint [LinearOrder ι]
+    {f : ι → Set α} (h : ¬ s.PairwiseDisjoint f) :
+    ∃ i ∈ s, ∃ j ∈ s, ∃ (_hij : i < j) (x : α), x ∈ f i ∩ f j := by
+  obtain ⟨i, hi, j, hj, hne, x, hx₁, hx₂⟩ := exists_ne_mem_inter_of_not_pairwiseDisjoint h
+  cases' lt_or_lt_iff_ne.mpr hne with h_lt h_lt
+  · exact ⟨i, hi, j, hj, h_lt, x, hx₁, hx₂⟩
+  · exact ⟨j, hj, i, hi, h_lt, x, hx₂, hx₁⟩
+
 end Set
 
+lemma exists_ne_mem_inter_of_not_pairwise_disjoint
+    {f : ι → Set α} (h : ¬ Pairwise (Disjoint on f)) :
+    ∃ (i j : ι) (_hij : i ≠ j) (x : α), x ∈ f i ∩ f j := by
+  rw [← pairwise_univ] at h
+  obtain ⟨i, _hi, j, _hj, h⟩ := exists_ne_mem_inter_of_not_pairwiseDisjoint h
+  exact ⟨i, j, h⟩
+
+lemma exists_lt_mem_inter_of_not_pairwise_disjoint [LinearOrder ι]
+    {f : ι → Set α} (h : ¬ Pairwise (Disjoint on f)) :
+    ∃ (i j : ι) (_ : i < j) (x : α), x ∈ f i ∩ f j := by
+  rw [← pairwise_univ] at h
+  obtain ⟨i, _hi, j, _hj, h⟩ := exists_lt_mem_inter_of_not_pairwiseDisjoint h
+  exact ⟨i, j, h⟩
+
 theorem pairwise_disjoint_fiber (f : ι → α) : Pairwise (Disjoint on fun a : α => f ⁻¹' {a}) :=
   pairwise_univ.1 <| Set.pairwiseDisjoint_fiber f univ
 #align pairwise_disjoint_fiber pairwise_disjoint_fiber

Mathlib/Topology/ContinuousFunction/Weierstrass.lean

@@ -53,7 +53,7 @@ so we may as well get this done first.)
 -/
 theorem polynomialFunctions_closure_eq_top (a b : ℝ) :
     (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤ := by
-  by_cases h : a < b
+  cases' lt_or_le a b with h h
   -- (Otherwise it's easy; we'll deal with that later.)
   · -- We can pullback continuous functions on `[a,b]` to continuous functions on `[0,1]`,
     -- by precomposing with an affine map.
@@ -75,11 +75,7 @@ theorem polynomialFunctions_closure_eq_top (a b : ℝ) :
     -- 🎉
     exact p
   · -- Otherwise, `b ≤ a`, and the interval is a subsingleton,
-    -- so all subalgebras are the same anyway.
-    haveI : Subsingleton (Set.Icc a b) :=
-      ⟨fun x y =>
-        le_antisymm ((x.2.2.trans (not_lt.mp h)).trans y.2.1)
-          ((y.2.2.trans (not_lt.mp h)).trans x.2.1)⟩
+    have : Subsingleton (Set.Icc a b) := (Set.subsingleton_coe _).mpr $ Set.subsingleton_Icc_of_ge h
     apply Subsingleton.elim
 #align polynomial_functions_closure_eq_top polynomialFunctions_closure_eq_top