chore: move basic lemmas to basic files (#1109)

synchronize with leanprover-community/mathlib#17882

~~Make `disjoint_singleton` `@[simp 1100]` because the linter complains it is not in simpNF (because of `disjoint_singleton_left` and `disjoint_singleton_right`).~~

Removing `simp` of `disjoint_singleton`, making `disjoint_singleton_left` have a greater priority than `disjoint_singleton_right`, then `disjoint_singleton` can be proved by `simp`.

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 1b36dabc50929b36caec16306358a5cc44ab441e
+! leanprover-community/mathlib commit 3d95492390dc90e34184b13e865f50bc67f30fbb
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -2754,3 +2754,203 @@ instance decidableSetOf (p : α → Prop) [Decidable (p a)] : Decidable (a ∈ {
 #align set.decidable_set_of Set.decidableSetOf
 
 end Set
+
+/-! ### Monotone lemmas for sets -/
+
+section Monotone
+variable {α β : Type _}
+
+theorem Monotone.inter [Preorder β] {f g : β → Set α} (hf : Monotone f) (hg : Monotone g) :
+    Monotone fun x => f x ∩ g x :=
+  hf.inf hg
+#align monotone.inter Monotone.inter
+
+theorem MonotoneOn.inter [Preorder β] {f g : β → Set α} {s : Set β} (hf : MonotoneOn f s)
+    (hg : MonotoneOn g s) : MonotoneOn (fun x => f x ∩ g x) s :=
+  hf.inf hg
+#align monotone_on.inter MonotoneOn.inter
+
+theorem Antitone.inter [Preorder β] {f g : β → Set α} (hf : Antitone f) (hg : Antitone g) :
+    Antitone fun x => f x ∩ g x :=
+  hf.inf hg
+#align antitone.inter Antitone.inter
+
+theorem AntitoneOn.inter [Preorder β] {f g : β → Set α} {s : Set β} (hf : AntitoneOn f s)
+    (hg : AntitoneOn g s) : AntitoneOn (fun x => f x ∩ g x) s :=
+  hf.inf hg
+#align antitone_on.inter AntitoneOn.inter
+
+theorem Monotone.union [Preorder β] {f g : β → Set α} (hf : Monotone f) (hg : Monotone g) :
+    Monotone fun x => f x ∪ g x :=
+  hf.sup hg
+#align monotone.union Monotone.union
+
+theorem MonotoneOn.union [Preorder β] {f g : β → Set α} {s : Set β} (hf : MonotoneOn f s)
+    (hg : MonotoneOn g s) : MonotoneOn (fun x => f x ∪ g x) s :=
+  hf.sup hg
+#align monotone_on.union MonotoneOn.union
+
+theorem Antitone.union [Preorder β] {f g : β → Set α} (hf : Antitone f) (hg : Antitone g) :
+    Antitone fun x => f x ∪ g x :=
+  hf.sup hg
+#align antitone.union Antitone.union
+
+theorem AntitoneOn.union [Preorder β] {f g : β → Set α} {s : Set β} (hf : AntitoneOn f s)
+    (hg : AntitoneOn g s) : AntitoneOn (fun x => f x ∪ g x) s :=
+  hf.sup hg
+#align antitone_on.union AntitoneOn.union
+
+namespace Set
+
+theorem monotone_setOf [Preorder α] {p : α → β → Prop} (hp : ∀ b, Monotone fun a => p a b) :
+    Monotone fun a => { b | p a b } := fun _ _ h b => hp b h
+#align set.monotone_set_of Set.monotone_setOf
+
+theorem antitone_setOf [Preorder α] {p : α → β → Prop} (hp : ∀ b, Antitone fun a => p a b) :
+    Antitone fun a => { b | p a b } := fun _ _ h b => hp b h
+#align set.antitone_set_of Set.antitone_setOf
+
+/-- Quantifying over a set is antitone in the set -/
+theorem antitone_bforall {P : α → Prop} : Antitone fun s : Set α => ∀ x ∈ s, P x :=
+  fun _ _ hst h x hx => h x <| hst hx
+#align set.antitone_bforall Set.antitone_bforall
+
+end Set
+
+end Monotone
+
+/-! ### Disjoint sets -/
+
+section Disjoint
+
+variable {α β : Type _} {s t u : Set α} {f : α → β}
+
+namespace Disjoint
+
+theorem union_left (hs : Disjoint s u) (ht : Disjoint t u) : Disjoint (s ∪ t) u :=
+  hs.sup_left ht
+#align disjoint.union_left Disjoint.union_left
+
+theorem union_right (ht : Disjoint s t) (hu : Disjoint s u) : Disjoint s (t ∪ u) :=
+  ht.sup_right hu
+#align disjoint.union_right Disjoint.union_right
+
+theorem inter_left (u : Set α) (h : Disjoint s t) : Disjoint (s ∩ u) t :=
+  h.inf_left _
+#align disjoint.inter_left Disjoint.inter_left
+
+theorem inter_left' (u : Set α) (h : Disjoint s t) : Disjoint (u ∩ s) t :=
+  h.inf_left' _
+#align disjoint.inter_left' Disjoint.inter_left'
+
+theorem inter_right (u : Set α) (h : Disjoint s t) : Disjoint s (t ∩ u) :=
+  h.inf_right _
+#align disjoint.inter_right Disjoint.inter_right
+
+theorem inter_right' (u : Set α) (h : Disjoint s t) : Disjoint s (u ∩ t) :=
+  h.inf_right' _
+#align disjoint.inter_right' Disjoint.inter_right'
+
+theorem subset_left_of_subset_union (h : s ⊆ t ∪ u) (hac : Disjoint s u) : s ⊆ t :=
+  hac.left_le_of_le_sup_right h
+#align disjoint.subset_left_of_subset_union Disjoint.subset_left_of_subset_union
+
+theorem subset_right_of_subset_union (h : s ⊆ t ∪ u) (hab : Disjoint s t) : s ⊆ u :=
+  hab.left_le_of_le_sup_left h
+#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/Function.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Andrew Zipperer, Haitao Zhang, Minchao Wu, Yury Kudryashov
 
 ! This file was ported from Lean 3 source module data.set.function
-! leanprover-community/mathlib commit 198161d833f2c01498c39c266b0b3dbe2c7a8c07
+! leanprover-community/mathlib commit 3d95492390dc90e34184b13e865f50bc67f30fbb
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -538,6 +538,24 @@ theorem range_restrictPreimage : range (t.restrictPreimage f) = Subtype.val ⁻
     Subtype.coe_preimage_self, Set.univ_inter]
 #align set.range_restrict_preimage Set.range_restrictPreimage
 
+variable {f} {U : ι → Set β}
+
+lemma restrictPreimage_injective (hf : Injective f) : Injective (t.restrictPreimage f) :=
+  fun _ _ e => Subtype.coe_injective <| hf <| Subtype.mk.inj e
+#align set.restrict_preimage_injective Set.restrictPreimage_injective
+
+lemma restrictPreimage_surjective (hf : Surjective f) : Surjective (t.restrictPreimage f) :=
+  fun x => ⟨⟨_, ((hf x).choose_spec.symm ▸ x.2 : _ ∈ t)⟩, Subtype.ext (hf x).choose_spec⟩
+#align set.restrict_preimage_surjective Set.restrictPreimage_surjective
+
+lemma restrictPreimage_bijective (hf : Bijective f) : Bijective (t.restrictPreimage f) :=
+  ⟨t.restrictPreimage_injective hf.1, t.restrictPreimage_surjective hf.2⟩
+#align set.restrict_preimage_bijective Set.restrictPreimage_bijective
+
+alias Set.restrictPreimage_injective  ← _root_.Function.Injective.restrictPreimage
+alias Set.restrictPreimage_surjective ← _root_.Function.Surjective.restrictPreimage
+alias Set.restrictPreimage_bijective  ← _root_.Function.Bijective.restrictPreimage
+
 end
 
 /-! ### Injectivity on a set -/
@@ -672,6 +690,23 @@ theorem InjOn.cancel_left (hg : t.InjOn g) (hf₁ : s.MapsTo f₁ t) (hf₂ : s.
   ⟨fun h => h.cancel_left hg hf₁ hf₂, EqOn.comp_left⟩
 #align set.inj_on.cancel_left Set.InjOn.cancel_left
 
+lemma InjOn.image_inter {s t u : Set α} (hf : u.InjOn f) (hs : s ⊆ u) (ht : t ⊆ u) :
+    f '' (s ∩ t) = f '' s ∩ f '' t := by
+  apply Subset.antisymm (image_inter_subset _ _ _)
+  intro x ⟨⟨y, ys, hy⟩, ⟨z, zt, hz⟩⟩
+  have : y = z := by
+    apply hf (hs ys) (ht zt)
+    rwa [← hz] at hy
+  rw [← this] at zt
+  exact ⟨y, ⟨ys, zt⟩, hy⟩
+#align set.inj_on.image_inter Set.InjOn.image_inter
+
+theorem _root_.Disjoint.image {s t u : Set α} {f : α → β} (h : Disjoint s t) (hf : u.InjOn f)
+    (hs : s ⊆ u) (ht : t ⊆ u) : Disjoint (f '' s) (f '' t) := by
+  rw [disjoint_iff_inter_eq_empty] at h ⊢
+  rw [← hf.image_inter hs ht, h, image_empty]
+#align disjoint.image Disjoint.image
+
 /-! ### Surjectivity on a set -/
 
 

Mathlib/Data/Set/Image.lean

@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura
 Ported by: Winston Yin
 
 ! This file was ported from Lean 3 source module data.set.image
-! leanprover-community/mathlib commit f178c0e25af359f6cbc72a96a243efd3b12423a3
+! leanprover-community/mathlib commit 3d95492390dc90e34184b13e865f50bc67f30fbb
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -302,6 +302,10 @@ theorem image_subset {a b : Set α} (f : α → β) (h : a ⊆ b) : f '' a ⊆ f
   exact fun x => fun ⟨w, h1, h2⟩ => ⟨w, h h1, h2⟩
 #align set.image_subset Set.image_subset
 
+/-- `Set.image` is monotone. See `Set.image_subset` for the statement in terms of `⊆`. -/
+lemma monotone_image {f : α → β} : Monotone (image f) := fun _ _ => image_subset _
+#align set.monotone_image Set.monotone_image
+
 theorem image_union (f : α → β) (s t : Set α) : f '' (s ∪ t) = f '' s ∪ f '' t :=
   ext fun x =>
     ⟨by rintro ⟨a, h | h, rfl⟩ <;> [left, right] <;> exact ⟨_, h, rfl⟩, by
@@ -1544,3 +1548,64 @@ theorem eq_preimage_iff_image_eq {f : α → β} (hf : Bijective f) {s t} : s =
 end ImagePreimage
 
 end Set
+
+/-! ### Disjoint lemmas for image and preimage -/
+
+section Disjoint
+variable {α β γ : Type _} {f : α → β} {s t : Set α}
+
+theorem Disjoint.preimage (f : α → β) {s t : Set β} (h : Disjoint s t) :
+    Disjoint (f ⁻¹' s) (f ⁻¹' t) :=
+  disjoint_iff_inf_le.mpr fun _ hx => h.le_bot hx
+#align disjoint.preimage Disjoint.preimage
+
+namespace Set
+
+theorem disjoint_image_image {f : β → α} {g : γ → α} {s : Set β} {t : Set γ}
+    (h : ∀ b ∈ s, ∀ c ∈ t, f b ≠ g c) : Disjoint (f '' s) (g '' t) :=
+  disjoint_iff_inf_le.mpr <| by rintro a ⟨⟨b, hb, eq⟩, c, hc, rfl⟩; exact h b hb c hc eq
+#align set.disjoint_image_image Set.disjoint_image_image
+
+theorem disjoint_image_of_injective (hf : Injective f) {s t : Set α} (hd : Disjoint s t) :
+    Disjoint (f '' s) (f '' t) :=
+  disjoint_image_image fun _ hx _ hy => hf.ne fun H => Set.disjoint_iff.1 hd ⟨hx, H.symm ▸ hy⟩
+#align set.disjoint_image_of_injective Set.disjoint_image_of_injective
+
+theorem _root_.Disjoint.of_image (h : Disjoint (f '' s) (f '' t)) : Disjoint s t :=
+  disjoint_iff_inf_le.mpr fun _ hx =>
+    disjoint_left.1 h (mem_image_of_mem _ hx.1) (mem_image_of_mem _ hx.2)
+#align disjoint.of_image Disjoint.of_image
+
+theorem disjoint_image_iff (hf : Injective f) : Disjoint (f '' s) (f '' t) ↔ Disjoint s t :=
+  ⟨Disjoint.of_image, disjoint_image_of_injective hf⟩
+#align set.disjoint_image_iff Set.disjoint_image_iff
+
+theorem _root_.Disjoint.of_preimage (hf : Surjective f) {s t : Set β}
+    (h : Disjoint (f ⁻¹' s) (f ⁻¹' t)) : Disjoint s t := by
+  rw [disjoint_iff_inter_eq_empty, ← image_preimage_eq (_ ∩ _) hf, preimage_inter, h.inter_eq,
+    image_empty]
+#align disjoint.of_preimage Disjoint.of_preimage
+
+theorem disjoint_preimage_iff (hf : Surjective f) {s t : Set β} :
+    Disjoint (f ⁻¹' s) (f ⁻¹' t) ↔ Disjoint s t :=
+  ⟨Disjoint.of_preimage hf, Disjoint.preimage _⟩
+#align set.disjoint_preimage_iff Set.disjoint_preimage_iff
+
+theorem preimage_eq_empty {s : Set β} (h : Disjoint s (range f)) :
+    f ⁻¹' s = ∅ :=
+  by simpa using h.preimage f
+#align set.preimage_eq_empty Set.preimage_eq_empty
+
+theorem preimage_eq_empty_iff {s : Set β} : f ⁻¹' s = ∅ ↔ Disjoint s (range f) :=
+  ⟨fun h => by
+    simp only [eq_empty_iff_forall_not_mem, disjoint_iff_inter_eq_empty, not_exists, mem_inter_iff,
+      not_and, mem_range, mem_preimage] at h ⊢
+    intro y hy x hx
+    rw [← hx] at hy
+    exact h x hy,
+  preimage_eq_empty⟩
+#align set.preimage_eq_empty_iff Set.preimage_eq_empty_iff
+
+end Set
+
+end Disjoint