feat: A set is either a subsingleton or nontrivial (#1047)

Match leanprover-community/mathlib#17901 and leanprover-community/mathlib#17957

Mathlib/Data/Set/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
 
 ! This file was ported from Lean 3 source module data.set.basic
-! leanprover-community/mathlib commit 3d95492390dc90e34184b13e865f50bc67f30fbb
+! leanprover-community/mathlib commit b86832321b586c6ac23ef8cdef6a7a27e42b13bd
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -238,7 +238,7 @@ theorem Eq.subset {α} {s t : Set α} : s = t → s ⊆ t :=
 
 namespace Set
 
-variable {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} {a b : α} {s t u : Set α}
+variable {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} {a b : α} {s s₁ s₂ t t₁ t₂ u : Set α}
 
 -- Porting note: remove `noncomputable` later
 noncomputable instance : Inhabited (Set α) :=
@@ -1518,9 +1518,75 @@ theorem disjoint_left : Disjoint s t ↔ ∀ ⦃a⦄, a ∈ s → a ∉ t :=
   disjoint_iff_inf_le.trans <| forall_congr' fun _ => not_and
 #align set.disjoint_left Set.disjoint_left
 
-theorem disjoint_right : Disjoint s t ↔ ∀ ⦃a⦄, a ∈ t → a ∉ s := by rw [Disjoint.comm, disjoint_left]
+theorem disjoint_right : Disjoint s t ↔ ∀ ⦃a⦄, a ∈ t → a ∉ s := by rw [disjoint_comm, disjoint_left]
 #align set.disjoint_right Set.disjoint_right
 
+lemma not_disjoint_iff : ¬Disjoint s t ↔ ∃ x, x ∈ s ∧ x ∈ t :=
+  Set.disjoint_iff.not.trans $ not_forall.trans $ exists_congr fun _ ↦ not_not
+#align set.not_disjoint_iff Set.not_disjoint_iff
+
+lemma not_disjoint_iff_nonempty_inter : ¬ Disjoint s t ↔ (s ∩ t).Nonempty := not_disjoint_iff
+#align set.not_disjoint_iff_nonempty_inter Set.not_disjoint_iff_nonempty_inter
+
+alias not_disjoint_iff_nonempty_inter ↔ _ Nonempty.not_disjoint
+
+lemma disjoint_or_nonempty_inter (s t : Set α) : Disjoint s t ∨ (s ∩ t).Nonempty :=
+  (em _).imp_right not_disjoint_iff_nonempty_inter.1
+#align set.disjoint_or_nonempty_inter Set.disjoint_or_nonempty_inter
+
+lemma disjoint_iff_forall_ne : Disjoint s t ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ t → a ≠ b := by
+  simp only [Ne.def, disjoint_left, @imp_not_comm _ (_ = _), forall_eq']
+#align set.disjoint_iff_forall_ne Set.disjoint_iff_forall_ne
+
+alias disjoint_iff_forall_ne ↔ _root_.Disjoint.ne_of_mem _
+#align disjoint.ne_of_mem Disjoint.ne_of_mem
+
+lemma disjoint_of_subset_left (h : s ⊆ u) (d : Disjoint u t) : Disjoint s t := d.mono_left h
+#align set.disjoint_of_subset_left Set.disjoint_of_subset_left
+lemma disjoint_of_subset_right (h : t ⊆ u) (d : Disjoint s u) : Disjoint s t := d.mono_right h
+#align set.disjoint_of_subset_right Set.disjoint_of_subset_right
+
+lemma disjoint_of_subset (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) (h : Disjoint s₂ t₂) : Disjoint s₁ t₁ :=
+h.mono hs ht
+#align set.disjoint_of_subset Set.disjoint_of_subset
+
+@[simp]
+lemma disjoint_union_left : Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u := disjoint_sup_left
+#align set.disjoint_union_left Set.disjoint_union_left
+
+@[simp]
+lemma disjoint_union_right : Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u := disjoint_sup_right
+#align set.disjoint_union_right Set.disjoint_union_right
+
+@[simp] lemma disjoint_empty (s : Set α) : Disjoint s ∅ := disjoint_bot_right
+#align set.disjoint_empty Set.disjoint_empty
+@[simp] lemma empty_disjoint (s : Set α) : Disjoint ∅ s := disjoint_bot_left
+#align set.empty_disjoint Set.empty_disjoint
+
+@[simp] lemma univ_disjoint : Disjoint univ s ↔ s = ∅ := top_disjoint
+#align set.univ_disjoint Set.univ_disjoint
+@[simp] lemma disjoint_univ : Disjoint s univ ↔ s = ∅ := disjoint_top
+#align set.disjoint_univ Set.disjoint_univ
+
+lemma disjoint_sdiff_left : Disjoint (t \ s) s := disjoint_sdiff_self_left
+lemma disjoint_sdiff_right : Disjoint s (t \ s) := disjoint_sdiff_self_right
+
+@[simp default+1]
+lemma disjoint_singleton_left : Disjoint {a} s ↔ a ∉ s := by simp [Set.disjoint_iff, subset_def]
+#align set.disjoint_singleton_left Set.disjoint_singleton_left
+
+@[simp]
+lemma disjoint_singleton_right : Disjoint s {a} ↔ a ∉ s :=
+disjoint_comm.trans disjoint_singleton_left
+#align set.disjoint_singleton_right Set.disjoint_singleton_right
+
+lemma disjoint_singleton : Disjoint ({a} : Set α) {b} ↔ a ≠ b :=
+  by simp
+#align set.disjoint_singleton Set.disjoint_singleton
+
+lemma subset_diff : s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u := le_iff_subset.symm.trans le_sdiff
+#align set.subset_diff Set.subset_diff
+
 /-! ### Lemmas about complement -/
 
 
@@ -1940,14 +2006,9 @@ theorem diff_self_inter {s t : Set α} : s \ (s ∩ t) = s \ t :=
   sdiff_inf_self_left _ _
 #align set.diff_self_inter Set.diff_self_inter
 
-@[simp]
-theorem diff_eq_self {s t : Set α} : s \ t = s ↔ t ∩ s ⊆ ∅ :=
-  show s \ t = s ↔ t ⊓ s ≤ ⊥ from sdiff_eq_self_iff_disjoint.trans disjoint_iff_inf_le
-#align set.diff_eq_self Set.diff_eq_self
-
 @[simp]
 theorem diff_singleton_eq_self {a : α} {s : Set α} (h : a ∉ s) : s \ {a} = s :=
-  diff_eq_self.2 <| by simp [singleton_inter_eq_empty.2 h]
+sdiff_eq_self_iff_disjoint.2 $ by simp [h]
 #align set.diff_singleton_eq_self Set.diff_singleton_eq_self
 
 @[simp]
@@ -2505,6 +2566,22 @@ alias not_nontrivial_iff ↔ _ Subsingleton.not_nontrivial
 
 alias not_subsingleton_iff ↔ _ Nontrivial.not_subsingleton
 
+protected lemma subsingleton_or_nontrivial (s : Set α) : s.Subsingleton ∨ s.Nontrivial :=
+by simp [or_iff_not_imp_right]
+#align set.subsingleton_or_nontrivial Set.subsingleton_or_nontrivial
+
+lemma eq_singleton_or_nontrivial (ha : a ∈ s) : s = {a} ∨ s.Nontrivial :=
+by rw [←subsingleton_iff_singleton ha]; exact s.subsingleton_or_nontrivial
+#align set.eq_singleton_or_nontrivial Set.eq_singleton_or_nontrivial
+
+lemma nontrivial_iff_ne_singleton (ha : a ∈ s) : s.Nontrivial ↔ s ≠ {a} :=
+⟨Nontrivial.ne_singleton, (eq_singleton_or_nontrivial ha).resolve_left⟩
+#align set.nontrivial_iff_ne_singleton Set.nontrivial_iff_ne_singleton
+
+lemma Nonempty.exists_eq_singleton_or_nontrivial : s.Nonempty → (∃ a, s = {a}) ∨ s.Nontrivial :=
+fun ⟨a, ha⟩ ↦ (eq_singleton_or_nontrivial ha).imp_left $ Exists.intro a
+#align set.nonempty.exists_eq_singleton_or_nontrivial Set.Nonempty.exists_eq_singleton_or_nontrivial
+
 theorem univ_eq_true_false : univ = ({True, False} : Set Prop) :=
   Eq.symm <| eq_univ_of_forall <| fun x => by
     rw [mem_insert_iff, mem_singleton_iff]
@@ -2819,8 +2896,6 @@ end Monotone
 
 /-! ### Disjoint sets -/
 
-section Disjoint
-
 variable {α β : Type _} {s t u : Set α} {f : α → β}
 
 namespace Disjoint
@@ -2858,97 +2933,3 @@ theorem subset_right_of_subset_union (h : s ⊆ t ∪ u) (hab : Disjoint s t) :
 #align disjoint.subset_right_of_subset_union Disjoint.subset_right_of_subset_union
 
 end Disjoint
-
-namespace Set
-
-theorem not_disjoint_iff : ¬Disjoint s t ↔ ∃ x, x ∈ s ∧ x ∈ t :=
-  Set.disjoint_iff.not.trans <| not_forall.trans <| exists_congr fun _ => not_not
-#align set.not_disjoint_iff Set.not_disjoint_iff
-
-theorem not_disjoint_iff_nonempty_inter : ¬Disjoint s t ↔ (s ∩ t).Nonempty :=
-  not_disjoint_iff
-#align set.not_disjoint_iff_nonempty_inter Set.not_disjoint_iff_nonempty_inter
-
-alias not_disjoint_iff_nonempty_inter ↔ _ Nonempty.not_disjoint
-
-theorem disjoint_or_nonempty_inter (s t : Set α) : Disjoint s t ∨ (s ∩ t).Nonempty :=
-  (em _).imp_right not_disjoint_iff_nonempty_inter.mp
-#align set.disjoint_or_nonempty_inter Set.disjoint_or_nonempty_inter
-
-theorem disjoint_iff_forall_ne : Disjoint s t ↔ ∀ x ∈ s, ∀ y ∈ t, x ≠ y := by
-  simp only [Ne.def, disjoint_left, @imp_not_comm _ (_ = _), forall_eq']
-#align set.disjoint_iff_forall_ne Set.disjoint_iff_forall_ne
-
-theorem _root_.Disjoint.ne_of_mem (h : Disjoint s t) {x y} (hx : x ∈ s) (hy : y ∈ t) : x ≠ y :=
-  disjoint_iff_forall_ne.mp h x hx y hy
-#align disjoint.ne_of_mem Disjoint.ne_of_mem
-
-theorem disjoint_of_subset_left (h : s ⊆ u) (d : Disjoint u t) : Disjoint s t :=
-  d.mono_left h
-#align set.disjoint_of_subset_left Set.disjoint_of_subset_left
-
-theorem disjoint_of_subset_right (h : t ⊆ u) (d : Disjoint s u) : Disjoint s t :=
-  d.mono_right h
-#align set.disjoint_of_subset_right Set.disjoint_of_subset_right
-
-theorem disjoint_of_subset {s t u v : Set α} (h1 : s ⊆ u) (h2 : t ⊆ v) (d : Disjoint u v) :
-    Disjoint s t :=
-  d.mono h1 h2
-#align set.disjoint_of_subset Set.disjoint_of_subset
-
-@[simp]
-theorem disjoint_union_left : Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u :=
-  disjoint_sup_left
-#align set.disjoint_union_left Set.disjoint_union_left
-
-@[simp]
-theorem disjoint_union_right : Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u :=
-  disjoint_sup_right
-#align set.disjoint_union_right Set.disjoint_union_right
-
-theorem disjoint_diff {a b : Set α} : Disjoint a (b \ a) :=
-  disjoint_iff.2 (inter_diff_self _ _)
-#align set.disjoint_diff Set.disjoint_diff
-
-@[simp]
-theorem disjoint_empty (s : Set α) : Disjoint s ∅ :=
-  disjoint_bot_right
-#align set.disjoint_empty Set.disjoint_empty
-
-@[simp]
-theorem empty_disjoint (s : Set α) : Disjoint ∅ s :=
-  disjoint_bot_left
-#align set.empty_disjoint Set.empty_disjoint
-
-@[simp]
-theorem univ_disjoint {s : Set α} : Disjoint univ s ↔ s = ∅ :=
-  top_disjoint
-#align set.univ_disjoint Set.univ_disjoint
-
-@[simp]
-theorem disjoint_univ {s : Set α} : Disjoint s univ ↔ s = ∅ :=
-  disjoint_top
-#align set.disjoint_univ Set.disjoint_univ
-
-@[simp default+1]
-theorem disjoint_singleton_left {a : α} {s : Set α} : Disjoint {a} s ↔ a ∉ s :=
-  by simp [Set.disjoint_iff, subset_def]
-#align set.disjoint_singleton_left Set.disjoint_singleton_left
-
-@[simp]
-theorem disjoint_singleton_right {a : α} {s : Set α} : Disjoint s {a} ↔ a ∉ s :=
-  by rw [Disjoint.comm]; exact disjoint_singleton_left
-#align set.disjoint_singleton_right Set.disjoint_singleton_right
-
-theorem disjoint_singleton {a b : α} : Disjoint ({a} : Set α) {b} ↔ a ≠ b :=
-  by simp
-#align set.disjoint_singleton Set.disjoint_singleton
-
-theorem subset_diff {s t u : Set α} : s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u :=
-  ⟨fun h => ⟨fun _ hxs => (h hxs).1, disjoint_iff_inf_le.mpr fun _ ⟨hxs, hxu⟩ => (h hxs).2 hxu⟩,
-    fun ⟨h1, h2⟩ _ hxs => ⟨h1 hxs, fun hxu => h2.le_bot ⟨hxs, hxu⟩⟩⟩
-#align set.subset_diff Set.subset_diff
-
-end Set
-
-end Disjoint

Mathlib/Data/Set/Intervals/Disjoint.lean

@@ -60,7 +60,7 @@ theorem Ici_disjoint_Iic : Disjoint (Ici a) (Iic b) ↔ ¬a ≤ b := by
 
 @[simp]
 theorem Iic_disjoint_Ici : Disjoint (Iic a) (Ici b) ↔ ¬b ≤ a :=
-  Disjoint.comm.trans Ici_disjoint_Iic
+  disjoint_comm.trans Ici_disjoint_Iic
 #align set.Iic_disjoint_Ici Set.Iic_disjoint_Ici
 
 @[simp]

Mathlib/Data/Set/Lattice.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.set.lattice
-! leanprover-community/mathlib commit 3d95492390dc90e34184b13e865f50bc67f30fbb
+! leanprover-community/mathlib commit b86832321b586c6ac23ef8cdef6a7a27e42b13bd
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -449,14 +449,43 @@ theorem interᵢ_congr_of_surjective {f : ι → Set α} {g : ι₂ → Set α}
   h1.infᵢ_congr h h2
 #align set.Inter_congr_of_surjective Set.interᵢ_congr_of_surjective
 
-theorem unionᵢ_const [Nonempty ι] (s : Set β) : (⋃ _i : ι, s) = s :=
-  supᵢ_const
-#align set.Union_const Set.unionᵢ_const
+lemma unionᵢ_congr {s t : ι → Set α} (h : ∀ i, s i = t i) : (⋃ i, s i) = ⋃ i, t i := supᵢ_congr h
+#align set.Union_congr Set.unionᵢ_congr
+lemma interᵢ_congr {s t : ι → Set α} (h : ∀ i, s i = t i) : (⋂ i, s i) = ⋂ i, t i := infᵢ_congr h
+#align set.Inter_congr Set.interᵢ_congr
+
+/- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/
+/- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/
+lemma unionᵢ₂_congr {s t : ∀ i, κ i → Set α} (h : ∀ i j, s i j = t i j) :
+    (⋃ (i) (j), s i j) = ⋃ (i) (j), t i j :=
+  unionᵢ_congr fun i => unionᵢ_congr <| h i
+#align set.Union₂_congr Set.unionᵢ₂_congr
 
-theorem interᵢ_const [Nonempty ι] (s : Set β) : (⋂ _i : ι, s) = s :=
-  infᵢ_const
+/- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/
+/- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/
+lemma interᵢ₂_congr {s t : ∀ i, κ i → Set α} (h : ∀ i j, s i j = t i j) :
+    (⋂ (i) (j), s i j) = ⋂ (i) (j), t i j :=
+  interᵢ_congr fun i => interᵢ_congr <| h i
+#align set.Inter₂_congr Set.interᵢ₂_congr
+
+section Nonempty
+variable [Nonempty ι] {f : ι → Set α} {s : Set α}
+
+lemma unionᵢ_const (s : Set β) : (⋃ _i : ι, s) = s := supᵢ_const
+#align set.Union_const Set.unionᵢ_const
+lemma interᵢ_const (s : Set β) : (⋂ _i : ι, s) = s := infᵢ_const
 #align set.Inter_const Set.interᵢ_const
 
+lemma unionᵢ_eq_const (hf : ∀ i, f i = s) : (⋃ i, f i) = s :=
+(unionᵢ_congr hf).trans $ unionᵢ_const _
+#align set.Union_eq_const Set.unionᵢ_eq_const
+
+lemma interᵢ_eq_const (hf : ∀ i, f i = s) : (⋂ i, f i) = s :=
+(interᵢ_congr hf).trans $ interᵢ_const _
+#align set.Inter_eq_const Set.interᵢ_eq_const
+
+end Nonempty
+
 @[simp]
 theorem compl_unionᵢ (s : ι → Set β) : (⋃ i, s i)ᶜ = ⋂ i, s iᶜ :=
   compl_supᵢ
@@ -864,28 +893,6 @@ theorem binterᵢ_mono {s s' : Set α} {t t' : α → Set β} (hs : s ⊆ s') (h
   (binterᵢ_subset_binterᵢ_left hs).trans <| interᵢ₂_mono h
 #align set.bInter_mono Set.binterᵢ_mono
 
-theorem unionᵢ_congr {s t : ι → Set α} (h : ∀ i, s i = t i) : (⋃ i, s i) = ⋃ i, t i :=
-  supᵢ_congr h
-#align set.Union_congr Set.unionᵢ_congr
-
-theorem interᵢ_congr {s t : ι → Set α} (h : ∀ i, s i = t i) : (⋂ i, s i) = ⋂ i, t i :=
-  infᵢ_congr h
-#align set.Inter_congr Set.interᵢ_congr
-
-/- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/
-theorem unionᵢ₂_congr {s t : ∀ i, κ i → Set α} (h : ∀ i j, s i j = t i j) :
-    (⋃ (i) (j), s i j) = ⋃ (i) (j), t i j :=
-  unionᵢ_congr fun i => unionᵢ_congr <| h i
-#align set.Union₂_congr Set.unionᵢ₂_congr
-
-/- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/
-theorem interᵢ₂_congr {s t : ∀ i, κ i → Set α} (h : ∀ i j, s i j = t i j) :
-    (⋂ (i) (j), s i j) = ⋂ (i) (j), t i j :=
-  interᵢ_congr fun i => interᵢ_congr <| h i
-#align set.Inter₂_congr Set.interᵢ₂_congr
-
 theorem bunionᵢ_eq_unionᵢ (s : Set α) (t : ∀ x ∈ s, Set β) :
     (⋃ x ∈ s, t x ‹_›) = ⋃ x : s, t x x.2 :=
   supᵢ_subtype'

Mathlib/Logic/Equiv/Embedding.lean

@@ -79,7 +79,7 @@ def prodEmbeddingDisjointEquivSigmaEmbeddingRestricted {α β γ : Type _} :
     Equiv.sigmaCongrRight fun a =>
       (subtypeEquivProp <| by
             ext f
-            rw [← Set.range_subset_iff, Set.subset_compl_iff_disjoint_right, Disjoint.comm]).trans
+            rw [← Set.range_subset_iff, Set.subset_compl_iff_disjoint_right, disjoint_comm]).trans
         (codRestrict _ _)
 #align
   equiv.prod_embedding_disjoint_equiv_sigma_embedding_restricted

Mathlib/Order/BooleanAlgebra.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Bryan Gin-ge Chen
 
 ! This file was ported from Lean 3 source module order.boolean_algebra
-! leanprover-community/mathlib commit 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3
+! leanprover-community/mathlib commit bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -222,6 +222,13 @@ theorem disjoint_sdiff_self_right : Disjoint x (y \ x) :=
   disjoint_iff_inf_le.mpr inf_sdiff_self_right.le
 #align disjoint_sdiff_self_right disjoint_sdiff_self_right
 
+lemma le_sdiff : x ≤ y \ z ↔ x ≤ y ∧ Disjoint x z :=
+⟨fun h ↦ ⟨h.trans sdiff_le, disjoint_sdiff_self_left.mono_left h⟩, fun h ↦
+  by rw [←h.2.sdiff_eq_left]; exact sdiff_le_sdiff_right h.1⟩
+
+@[simp] lemma sdiff_eq_left : x \ y = x ↔ Disjoint x y :=
+⟨fun h ↦ disjoint_sdiff_self_left.mono_left h.ge, Disjoint.sdiff_eq_left⟩
+
 /- TODO: we could make an alternative constructor for `GeneralizedBooleanAlgebra` using
 `Disjoint x (y \ x)` and `x ⊔ (y \ x) = y` as axioms. -/
 theorem Disjoint.sdiff_eq_of_sup_eq (hi : Disjoint x z) (hs : x ⊔ z = y) : y \ x = z :=
@@ -312,7 +319,7 @@ theorem sdiff_eq_self_iff_disjoint : x \ y = x ↔ Disjoint y x :=
 #align sdiff_eq_self_iff_disjoint sdiff_eq_self_iff_disjoint
 
 theorem sdiff_eq_self_iff_disjoint' : x \ y = x ↔ Disjoint x y := by
-  rw [sdiff_eq_self_iff_disjoint, Disjoint.comm]
+  rw [sdiff_eq_self_iff_disjoint, disjoint_comm]
 #align sdiff_eq_self_iff_disjoint' sdiff_eq_self_iff_disjoint'
 
 theorem sdiff_lt (hx : y ≤ x) (hy : y ≠ ⊥) : x \ y < x := by

Mathlib/Order/CompleteBooleanAlgebra.lean

@@ -134,7 +134,7 @@ theorem supᵢ_disjoint_iff {f : ι → α} : Disjoint (⨆ i, f i) a ↔ ∀ i,
 #align supr_disjoint_iff supᵢ_disjoint_iff
 
 theorem disjoint_supᵢ_iff {f : ι → α} : Disjoint a (⨆ i, f i) ↔ ∀ i, Disjoint a (f i) := by
-  simpa only [Disjoint.comm] using @supᵢ_disjoint_iff
+  simpa only [disjoint_comm] using @supᵢ_disjoint_iff
 #align disjoint_supr_iff disjoint_supᵢ_iff
 
 theorem supᵢ₂_disjoint_iff {f : ∀ i, κ i → α} :
@@ -152,7 +152,7 @@ theorem supₛ_disjoint_iff {s : Set α} : Disjoint (supₛ s) a ↔ ∀ b ∈ s
 #align Sup_disjoint_iff supₛ_disjoint_iff
 
 theorem disjoint_supₛ_iff {s : Set α} : Disjoint a (supₛ s) ↔ ∀ b ∈ s, Disjoint a b := by
-  simpa only [Disjoint.comm] using @supₛ_disjoint_iff
+  simpa only [disjoint_comm] using @supₛ_disjoint_iff
 #align disjoint_Sup_iff disjoint_supₛ_iff
 
 theorem supᵢ_inf_of_monotone {ι : Type _} [Preorder ι] [IsDirected ι (· ≤ ·)] {f g : ι → α}