chore(data/set/pairwise): split (#17880)

This PR will split most of the lemmas in `data.set.pairwise` which are independent of the `data.set.lattice`. It makes a lot of files no longer depend on `data.set.lattice`.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20progress/near/315072418)

mathlib4 PR: leanprover-community/mathlib4#1184



Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

src/algebra/big_operators/basic.lean

@@ -3,7 +3,6 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-
 import algebra.big_operators.multiset.lemmas
 import algebra.group.pi
 import algebra.group_power.lemmas
@@ -13,7 +12,7 @@ import data.finset.sum
 import data.fintype.basic
 import data.finset.sigma
 import data.multiset.powerset
-import data.set.pairwise
+import data.set.pairwise.basic
 
 /-!
 # Big operators

src/data/finset/option.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Mario Carneiro, Sean Leather
 -/
 import data.finset.card
-import order.hom.basic
 
 /-!
 # Finite sets in `option α`

src/data/list/nodup.lean

@@ -6,7 +6,7 @@ Authors: Mario Carneiro, Kenny Lau
 import data.list.lattice
 import data.list.pairwise
 import data.list.forall2
-import data.set.pairwise
+import data.set.pairwise.basic
 
 /-!
 # Lists with no duplicates

src/data/multiset/finset_ops.lean

@@ -210,3 +210,7 @@ theorem ndinter_eq_zero_iff_disjoint {s t : multiset α} : ndinter s t = 0 ↔ d
 by rw ← subset_zero; simp [subset_iff, disjoint]
 
 end multiset
+
+-- Assert that we define `finset` without the material on the set lattice.
+-- Note that we cannot put this in `data.finset.basic` because we proved relevant lemmas there.
+assert_not_exists set.sInter

src/data/prod/tprod.lean

@@ -144,7 +144,7 @@ end
 lemma elim_preimage_pi [decidable_eq ι] {l : list ι} (hnd : l.nodup) (h : ∀ i, i ∈ l)
   (t : Π i, set (α i)) : tprod.elim' h ⁻¹' pi univ t = set.tprod l t :=
 begin
-  have : { i | i ∈ l} = univ, { ext i, simp [h] },
+  have : { i | i ∈ l } = univ, { ext i, simp [h] },
   rw [← this, ← mk_preimage_tprod, preimage_preimage],
   convert preimage_id, simp [tprod.mk_elim hnd h, id_def]
 end

src/data/set/intervals/group.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot, Yury Kudryashov, Rémy Degenne
 -/
 import data.set.intervals.basic
-import data.set.pairwise
+import data.set.pairwise.basic
 import algebra.order.group.abs
 import algebra.group_power.lemmas
 

src/data/set/pairwise.lean → src/data/set/pairwise/basic.lean

@@ -3,9 +3,9 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
+import data.set.function
 import logic.relation
 import logic.pairwise
-import data.set.lattice
 
 /-!
 # Relations holding pairwise
@@ -16,7 +16,7 @@ import data.set.lattice
 This file develops pairwise relations and defines pairwise disjoint indexed sets.
 
 We also prove many basic facts about `pairwise`. It is possible that an intermediate file,
-with more imports than `logic.pairwise` but not importing `data.set.lattice` would be appropriate
+with more imports than `logic.pairwise` but not importing `data.set.function` would be appropriate
 to hold many of these basic facts.
 
 ## Main declarations
@@ -56,8 +56,6 @@ lemma pairwise_disjoint.mono [semilattice_inf α] [order_bot α]
   (hs : pairwise (disjoint on f)) (h : g ≤ f) : pairwise (disjoint on g) :=
 hs.mono (λ i j hij, disjoint.mono (h i) (h j) hij)
 
-alias function.injective_iff_pairwise_ne ↔ function.injective.pairwise_ne _
-
 namespace set
 
 lemma pairwise.mono (h : t ⊆ s) (hs : s.pairwise r) : t.pairwise r :=
@@ -188,23 +186,6 @@ lemma inj_on.pairwise_image {s : set ι} (h : s.inj_on f) :
   (f '' s).pairwise r ↔ s.pairwise (r on f) :=
 by simp [h.eq_iff, set.pairwise] {contextual := tt}
 
-lemma pairwise_Union {f : ι → set α} (h : directed (⊆) f) :
-  (⋃ n, f n).pairwise r ↔ ∀ n, (f n).pairwise r :=
-begin
-  split,
-  { assume H n,
-    exact pairwise.mono (subset_Union _ _) H },
-  { assume H i hi j hj hij,
-    rcases mem_Union.1 hi with ⟨m, hm⟩,
-    rcases mem_Union.1 hj with ⟨n, hn⟩,
-    rcases h m n with ⟨p, mp, np⟩,
-    exact H p (mp hm) (np hn) hij }
-end
-
-lemma pairwise_sUnion {r : α → α → Prop} {s : set (set α)} (h : directed_on (⊆) s) :
-  (⋃₀ s).pairwise r ↔ (∀ a ∈ s, set.pairwise a r) :=
-by { rw [sUnion_eq_Union, pairwise_Union (h.directed_coe), set_coe.forall], refl }
-
 end set
 
 end pairwise
@@ -290,14 +271,6 @@ lemma pairwise_disjoint.union (hs : s.pairwise_disjoint f) (ht : t.pairwise_disj
   (s ∪ t).pairwise_disjoint f :=
 pairwise_disjoint_union.2 ⟨hs, ht, h⟩
 
-lemma pairwise_disjoint_Union {g : ι' → set ι} (h : directed (⊆) g) :
-  (⋃ n, g n).pairwise_disjoint f ↔ ∀ ⦃n⦄, (g n).pairwise_disjoint f :=
-pairwise_Union h
-
-lemma pairwise_disjoint_sUnion {s : set (set ι)} (h : directed_on (⊆) s) :
-  (⋃₀ s).pairwise_disjoint f ↔ ∀ ⦃a⦄, a ∈ s → set.pairwise_disjoint a f :=
-pairwise_sUnion h
-
 -- classical
 lemma pairwise_disjoint.elim (hs : s.pairwise_disjoint f) {i j : ι} (hi : i ∈ s) (hj : j ∈ s)
   (h : ¬ disjoint (f i) (f j)) :
@@ -321,27 +294,6 @@ hs.elim' hi hj $ λ h, hf $ (inf_of_le_left hij).symm.trans h
 
 end semilattice_inf_bot
 
-section complete_lattice
-variables [complete_lattice α]
-
-/-- Bind operation for `set.pairwise_disjoint`. If you want to only consider finsets of indices, you
-can use `set.pairwise_disjoint.bUnion_finset`. -/
-lemma pairwise_disjoint.bUnion {s : set ι'} {g : ι' → set ι} {f : ι → α}
-  (hs : s.pairwise_disjoint (λ i' : ι', ⨆ i ∈ g i', f i))
-  (hg : ∀ i ∈ s, (g i).pairwise_disjoint f) :
-  (⋃ i ∈ s, g i).pairwise_disjoint f :=
-begin
-  rintro a ha b hb hab,
-  simp_rw set.mem_Union at ha hb,
-  obtain ⟨c, hc, ha⟩ := ha,
-  obtain ⟨d, hd, hb⟩ := hb,
-  obtain hcd | hcd := eq_or_ne (g c) (g d),
-  { exact hg d hd (hcd.subst ha) hb hab },
-  { exact (hs hc hd $ ne_of_apply_ne _ hcd).mono (le_supr₂ a ha) (le_supr₂ b hb) }
-end
-
-end complete_lattice
-
 /-! ### Pairwise disjoint set of sets -/
 
 lemma pairwise_disjoint_range_singleton :
@@ -359,22 +311,6 @@ lemma pairwise_disjoint.elim_set {s : set ι} {f : ι → set α} (hs : s.pairwi
   (hi : i ∈ s) (hj : j ∈ s) (a : α) (hai : a ∈ f i) (haj : a ∈ f j) : i = j :=
 hs.elim hi hj $ not_disjoint_iff.2 ⟨a, hai, haj⟩
 
-lemma bUnion_diff_bUnion_eq {s t : set ι} {f : ι → set α} (h : (s ∪ t).pairwise_disjoint f) :
-  (⋃ i ∈ s, f i) \ (⋃ i ∈ t, f i) = (⋃ i ∈ s \ t, f i) :=
-begin
-  refine (bUnion_diff_bUnion_subset f s t).antisymm
-    (Union₂_subset $ λ i hi a ha, (mem_diff _).2 ⟨mem_bUnion hi.1 ha, _⟩),
-  rw mem_Union₂, rintro ⟨j, hj, haj⟩,
-  exact (h (or.inl hi.1) (or.inr hj) (ne_of_mem_of_not_mem hj hi.2).symm).le_bot ⟨ha, haj⟩,
-end
-
-/-- Equivalence between a disjoint bounded union and a dependent sum. -/
-noncomputable def bUnion_eq_sigma_of_disjoint {s : set ι} {f : ι → set α}
-  (h : s.pairwise_disjoint f) :
-  (⋃ i ∈ s, f i) ≃ (Σ i : s, f i) :=
-(equiv.set_congr (bUnion_eq_Union _ _)).trans $ Union_eq_sigma_of_disjoint $
-  λ ⟨i, hi⟩ ⟨j, hj⟩ ne, h hi hj $ λ eq, ne $ subtype.eq eq
-
 /-- The partial images of a binary function `f` whose partial evaluations are injective are pairwise
 disjoint iff `f` is injective . -/
 lemma pairwise_disjoint_image_right_iff {f : α → β → γ} {s : set α} {t : set β}
@@ -413,30 +349,3 @@ end set
 
 lemma pairwise_disjoint_fiber (f : ι → α) : pairwise (disjoint on (λ a : α, f ⁻¹' {a})) :=
 set.pairwise_univ.1 $ set.pairwise_disjoint_fiber f univ
-
-
-section
-variables {f : ι → set α} {s t : set ι}
-
-lemma set.pairwise_disjoint.subset_of_bUnion_subset_bUnion (h₀ : (s ∪ t).pairwise_disjoint f)
-  (h₁ : ∀ i ∈ s, (f i).nonempty) (h : (⋃ i ∈ s, f i) ⊆ ⋃ i ∈ t, f i) :
-  s ⊆ t :=
-begin
-  rintro i hi,
-  obtain ⟨a, hai⟩ := h₁ i hi,
-  obtain ⟨j, hj, haj⟩ := mem_Union₂.1 (h $ mem_Union₂_of_mem hi hai),
-  rwa h₀.eq (subset_union_left _ _ hi) (subset_union_right _ _ hj)
-    (not_disjoint_iff.2 ⟨a, hai, haj⟩),
-end
-
-lemma pairwise.subset_of_bUnion_subset_bUnion (h₀ : pairwise (disjoint on f))
-  (h₁ : ∀ i ∈ s, (f i).nonempty) (h : (⋃ i ∈ s, f i) ⊆ ⋃ i ∈ t, f i) :
-  s ⊆ t :=
-set.pairwise_disjoint.subset_of_bUnion_subset_bUnion (h₀.set_pairwise _) h₁ h
-
-lemma pairwise.bUnion_injective (h₀ : pairwise (disjoint on f)) (h₁ : ∀ i, (f i).nonempty) :
-  injective (λ s : set ι, ⋃ i ∈ s, f i) :=
-λ s t h, (h₀.subset_of_bUnion_subset_bUnion (λ _ _, h₁ _) $ h.subset).antisymm $
-  h₀.subset_of_bUnion_subset_bUnion (λ _ _, h₁ _) $ h.superset
-
-end

src/data/set/pairwise/lattice.lean

@@ -0,0 +1,123 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl
+-/
+import data.set.lattice
+import data.set.pairwise.basic
+
+/-!
+# Relations holding pairwise
+
+In this file we prove many facts about `pairwise` and the set lattice.
+-/
+
+open set function
+
+variables {α β γ ι ι' : Type*} {r p q : α → α → Prop}
+
+section pairwise
+variables {f g : ι → α} {s t u : set α} {a b : α}
+
+namespace set
+
+lemma pairwise_Union {f : ι → set α} (h : directed (⊆) f) :
+  (⋃ n, f n).pairwise r ↔ ∀ n, (f n).pairwise r :=
+begin
+  split,
+  { assume H n,
+    exact pairwise.mono (subset_Union _ _) H },
+  { assume H i hi j hj hij,
+    rcases mem_Union.1 hi with ⟨m, hm⟩,
+    rcases mem_Union.1 hj with ⟨n, hn⟩,
+    rcases h m n with ⟨p, mp, np⟩,
+    exact H p (mp hm) (np hn) hij }
+end
+
+lemma pairwise_sUnion {r : α → α → Prop} {s : set (set α)} (h : directed_on (⊆) s) :
+  (⋃₀ s).pairwise r ↔ (∀ a ∈ s, set.pairwise a r) :=
+by { rw [sUnion_eq_Union, pairwise_Union (h.directed_coe), set_coe.forall], refl }
+
+end set
+
+end pairwise
+
+namespace set
+section partial_order_bot
+variables [partial_order α] [order_bot α] {s t : set ι} {f g : ι → α}
+
+lemma pairwise_disjoint_Union {g : ι' → set ι} (h : directed (⊆) g) :
+  (⋃ n, g n).pairwise_disjoint f ↔ ∀ ⦃n⦄, (g n).pairwise_disjoint f :=
+pairwise_Union h
+
+lemma pairwise_disjoint_sUnion {s : set (set ι)} (h : directed_on (⊆) s) :
+  (⋃₀ s).pairwise_disjoint f ↔ ∀ ⦃a⦄, a ∈ s → set.pairwise_disjoint a f :=
+pairwise_sUnion h
+
+end partial_order_bot
+
+section complete_lattice
+variables [complete_lattice α]
+
+/-- Bind operation for `set.pairwise_disjoint`. If you want to only consider finsets of indices, you
+can use `set.pairwise_disjoint.bUnion_finset`. -/
+lemma pairwise_disjoint.bUnion {s : set ι'} {g : ι' → set ι} {f : ι → α}
+  (hs : s.pairwise_disjoint (λ i' : ι', ⨆ i ∈ g i', f i))
+  (hg : ∀ i ∈ s, (g i).pairwise_disjoint f) :
+  (⋃ i ∈ s, g i).pairwise_disjoint f :=
+begin
+  rintro a ha b hb hab,
+  simp_rw set.mem_Union at ha hb,
+  obtain ⟨c, hc, ha⟩ := ha,
+  obtain ⟨d, hd, hb⟩ := hb,
+  obtain hcd | hcd := eq_or_ne (g c) (g d),
+  { exact hg d hd (hcd.subst ha) hb hab },
+  { exact (hs hc hd $ ne_of_apply_ne _ hcd).mono (le_supr₂ a ha) (le_supr₂ b hb) }
+end
+
+end complete_lattice
+
+lemma bUnion_diff_bUnion_eq {s t : set ι} {f : ι → set α} (h : (s ∪ t).pairwise_disjoint f) :
+  (⋃ i ∈ s, f i) \ (⋃ i ∈ t, f i) = (⋃ i ∈ s \ t, f i) :=
+begin
+  refine (bUnion_diff_bUnion_subset f s t).antisymm
+    (Union₂_subset $ λ i hi a ha, (mem_diff _).2 ⟨mem_bUnion hi.1 ha, _⟩),
+  rw mem_Union₂, rintro ⟨j, hj, haj⟩,
+  exact (h (or.inl hi.1) (or.inr hj) (ne_of_mem_of_not_mem hj hi.2).symm).le_bot ⟨ha, haj⟩,
+end
+
+/-- Equivalence between a disjoint bounded union and a dependent sum. -/
+noncomputable def bUnion_eq_sigma_of_disjoint {s : set ι} {f : ι → set α}
+  (h : s.pairwise_disjoint f) :
+  (⋃ i ∈ s, f i) ≃ (Σ i : s, f i) :=
+(equiv.set_congr (bUnion_eq_Union _ _)).trans $ Union_eq_sigma_of_disjoint $
+  λ ⟨i, hi⟩ ⟨j, hj⟩ ne, h hi hj $ λ eq, ne $ subtype.eq eq
+
+end set
+
+
+section
+variables {f : ι → set α} {s t : set ι}
+
+lemma set.pairwise_disjoint.subset_of_bUnion_subset_bUnion (h₀ : (s ∪ t).pairwise_disjoint f)
+  (h₁ : ∀ i ∈ s, (f i).nonempty) (h : (⋃ i ∈ s, f i) ⊆ ⋃ i ∈ t, f i) :
+  s ⊆ t :=
+begin
+  rintro i hi,
+  obtain ⟨a, hai⟩ := h₁ i hi,
+  obtain ⟨j, hj, haj⟩ := mem_Union₂.1 (h $ mem_Union₂_of_mem hi hai),
+  rwa h₀.eq (subset_union_left _ _ hi) (subset_union_right _ _ hj)
+    (not_disjoint_iff.2 ⟨a, hai, haj⟩),
+end
+
+lemma pairwise.subset_of_bUnion_subset_bUnion (h₀ : pairwise (disjoint on f))
+  (h₁ : ∀ i ∈ s, (f i).nonempty) (h : (⋃ i ∈ s, f i) ⊆ ⋃ i ∈ t, f i) :
+  s ⊆ t :=
+set.pairwise_disjoint.subset_of_bUnion_subset_bUnion (h₀.set_pairwise _) h₁ h
+
+lemma pairwise.bUnion_injective (h₀ : pairwise (disjoint on f)) (h₁ : ∀ i, (f i).nonempty) :
+  injective (λ s : set ι, ⋃ i ∈ s, f i) :=
+λ s t h, (h₀.subset_of_bUnion_subset_bUnion (λ _ _, h₁ _) $ h.subset).antisymm $
+  h₀.subset_of_bUnion_subset_bUnion (λ _ _, h₁ _) $ h.superset
+
+end

src/data/set/pointwise/smul.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Floris van Doorn
 -/
 import algebra.module.basic
-import data.set.pairwise
+import data.set.pairwise.lattice
 import data.set.pointwise.basic
 import tactic.by_contra
 

src/order/antichain.lean

@@ -3,7 +3,10 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import data.set.pairwise
+import data.set.pairwise.basic
+import order.bounds.basic
+import order.directed
+import order.hom.set
 
 /-!
 # Antichains

src/order/chain.lean

@@ -3,7 +3,8 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import data.set.pairwise
+import data.set.pairwise.basic
+import data.set.lattice
 import data.set_like.basic
 
 /-!

src/order/succ_pred/interval_succ.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import data.set.pairwise
+import data.set.pairwise.basic
 import order.succ_pred.basic
 
 /-!