chore: Split data.set.pairwise (#3117)

Match leanprover-community/mathlib#17880

The new import of `Mathlib.Data.Set.Lattice` in `Mathlib.Data.Finset.Basic` was implied transitively from tactic imports present in Lean 3.



Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

Mathlib.lean

@@ -956,7 +956,8 @@ import Mathlib.Data.Set.Lattice
 import Mathlib.Data.Set.MulAntidiagonal
 import Mathlib.Data.Set.NAry
 import Mathlib.Data.Set.Opposite
-import Mathlib.Data.Set.Pairwise
+import Mathlib.Data.Set.Pairwise.Basic
+import Mathlib.Data.Set.Pairwise.Lattice
 import Mathlib.Data.Set.Pointwise.Basic
 import Mathlib.Data.Set.Pointwise.BigOperators
 import Mathlib.Data.Set.Pointwise.Finite

Mathlib/Algebra/BigOperators/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 
 ! This file was ported from Lean 3 source module algebra.big_operators.basic
-! leanprover-community/mathlib commit 6c5f73fd6f6cc83122788a80a27cdd54663609f4
+! leanprover-community/mathlib commit c227d107bbada5d0d9d20287e3282c0a7f1651a0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -17,7 +17,7 @@ import Mathlib.Data.Finset.Sum
 import Mathlib.Data.Fintype.Basic
 import Mathlib.Data.Finset.Sigma
 import Mathlib.Data.Multiset.Powerset
-import Mathlib.Data.Set.Pairwise
+import Mathlib.Data.Set.Pairwise.Basic
 import Mathlib.Tactic.ScopedNS
 
 /-!

Mathlib/Data/Finset/Basic.lean

@@ -9,6 +9,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Minchao Wu, Mario Carneiro
 ! if you have ported upstream changes.
 -/
 import Mathlib.Data.Multiset.FinsetOps
+import Mathlib.Data.Set.Lattice
 
 /-!
 # Finite sets

Mathlib/Data/Finset/Option.lean

@@ -4,12 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Mario Carneiro, Sean Leather
 
 ! This file was ported from Lean 3 source module data.finset.option
-! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
+! leanprover-community/mathlib commit c227d107bbada5d0d9d20287e3282c0a7f1651a0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathlib.Data.Finset.Card
-import Mathlib.Order.Hom.Basic
 
 /-!
 # Finite sets in `option α`

Mathlib/Data/List/Nodup.lean

@@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kenny Lau
 
 ! This file was ported from Lean 3 source module data.list.nodup
-! leanprover-community/mathlib commit f694c7dead66f5d4c80f446c796a5aad14707f0e
+! leanprover-community/mathlib commit c227d107bbada5d0d9d20287e3282c0a7f1651a0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathlib.Data.List.Lattice
 import Mathlib.Data.List.Pairwise
 import Mathlib.Data.List.Forall2
-import Mathlib.Data.Set.Pairwise
+import Mathlib.Data.Set.Pairwise.Basic
 
 /-!
 # Lists with no duplicates

Mathlib/Data/Multiset/FinsetOps.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.multiset.finset_ops
-! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
+! leanprover-community/mathlib commit c227d107bbada5d0d9d20287e3282c0a7f1651a0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -287,3 +287,8 @@ theorem ndinter_eq_zero_iff_disjoint {s t : Multiset α} : ndinter s t = 0 ↔ D
 #align multiset.ndinter_eq_zero_iff_disjoint Multiset.ndinter_eq_zero_iff_disjoint
 
 end Multiset
+
+-- Porting note: `assert_not_exists` has not been ported yet.
+-- -- 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

Mathlib/Data/Prod/TProd.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 
 ! This file was ported from Lean 3 source module data.prod.tprod
-! leanprover-community/mathlib commit 7b78d1776212a91ecc94cf601f83bdcc46b04213
+! leanprover-community/mathlib commit c227d107bbada5d0d9d20287e3282c0a7f1651a0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/

Mathlib/Data/Set/Intervals/Group.lean

@@ -5,12 +5,12 @@ Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot, Yury Kudryashov, Rémy
 Ported by: Winston Yin
 
 ! This file was ported from Lean 3 source module data.set.intervals.group
-! leanprover-community/mathlib commit 740acc0e6f9adf4423f92a485d0456fc271482da
+! leanprover-community/mathlib commit c227d107bbada5d0d9d20287e3282c0a7f1651a0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathlib.Data.Set.Intervals.Basic
-import Mathlib.Data.Set.Pairwise
+import Mathlib.Data.Set.Pairwise.Basic
 import Mathlib.Algebra.Order.Group.Abs
 import Mathlib.Algebra.GroupPower.Lemmas
 

Mathlib/Data/Set/Pairwise.lean → Mathlib/Data/Set/Pairwise/Basic.lean

@@ -3,22 +3,22 @@ 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
 
-! This file was ported from Lean 3 source module data.set.pairwise
-! leanprover-community/mathlib commit 207cfac9fcd06138865b5d04f7091e46d9320432
+! This file was ported from Lean 3 source module data.set.pairwise.basic
+! leanprover-community/mathlib commit c227d107bbada5d0d9d20287e3282c0a7f1651a0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
+import Mathlib.Data.Set.Function
 import Mathlib.Logic.Relation
 import Mathlib.Logic.Pairwise
-import Mathlib.Data.Set.Lattice
 
 /-!
 # Relations holding pairwise
 
 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
@@ -65,10 +65,6 @@ theorem pairwise_disjoint_mono [SemilatticeInf α] [OrderBot α] (hs : Pairwise
   hs.mono fun i j hij => Disjoint.mono (h i) (h j) hij
 #align pairwise_disjoint.mono pairwise_disjoint_mono
 
--- porting note:
--- alias Function.injective_iff_pairwise_ne ↔ Function.Injective.pairwise_ne _
--- is already present in Mathlib.Logic.Pairwise.
-
 namespace Set
 
 theorem Pairwise.mono (h : t ⊆ s) (hs : s.Pairwise r) : t.Pairwise r :=
@@ -221,23 +217,6 @@ theorem InjOn.pairwise_image {s : Set ι} (h : s.InjOn f) :
   simp (config := { contextual := true }) [h.eq_iff, Set.Pairwise]
 #align set.inj_on.pairwise_image Set.InjOn.pairwise_image
 
-theorem pairwise_unionᵢ {f : ι → Set α} (h : Directed (· ⊆ ·) f) :
-    (⋃ n, f n).Pairwise r ↔ ∀ n, (f n).Pairwise r := by
-  constructor
-  · intro H n
-    exact Pairwise.mono (subset_unionᵢ _ _) H
-  · intro 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
-#align set.pairwise_Union Set.pairwise_unionᵢ
-
-theorem pairwise_unionₛ {r : α → α → Prop} {s : Set (Set α)} (h : DirectedOn (· ⊆ ·) s) :
-    (⋃₀s).Pairwise r ↔ ∀ a ∈ s, Set.Pairwise a r := by
-  rw [unionₛ_eq_unionᵢ, pairwise_unionᵢ h.directed_val, SetCoe.forall]
-#align set.pairwise_sUnion Set.pairwise_unionₛ
-
 end Set
 
 end Pairwise
@@ -339,16 +318,6 @@ theorem PairwiseDisjoint.union (hs : s.PairwiseDisjoint f) (ht : t.PairwiseDisjo
   pairwiseDisjoint_union.2 ⟨hs, ht, h⟩
 #align set.pairwise_disjoint.union Set.PairwiseDisjoint.union
 
-theorem pairwiseDisjoint_unionᵢ {g : ι' → Set ι} (h : Directed (· ⊆ ·) g) :
-    (⋃ n, g n).PairwiseDisjoint f ↔ ∀ ⦃n⦄, (g n).PairwiseDisjoint f :=
-  pairwise_unionᵢ h
-#align set.pairwise_disjoint_Union Set.pairwiseDisjoint_unionᵢ
-
-theorem pairwiseDisjoint_unionₛ {s : Set (Set ι)} (h : DirectedOn (· ⊆ ·) s) :
-    (⋃₀s).PairwiseDisjoint f ↔ ∀ ⦃a⦄, a ∈ s → PairwiseDisjoint a f :=
-  pairwise_unionₛ h
-#align set.pairwise_disjoint_sUnion Set.pairwiseDisjoint_unionₛ
-
 -- classical
 theorem PairwiseDisjoint.elim (hs : s.PairwiseDisjoint f) {i j : ι} (hi : i ∈ s) (hj : j ∈ s)
     (h : ¬Disjoint (f i) (f j)) : i = j :=
@@ -374,29 +343,6 @@ theorem PairwiseDisjoint.eq_of_le (hs : s.PairwiseDisjoint f) {i j : ι} (hi : i
 
 end SemilatticeInfBot
 
-section CompleteLattice
-
-variable [CompleteLattice α]
-
-/-- Bind operation for `Set.PairwiseDisjoint`. If you want to only consider finsets of indices, you
-can use `Set.PairwiseDisjoint.bunionᵢ_finset`. -/
-theorem PairwiseDisjoint.bunionᵢ {s : Set ι'} {g : ι' → Set ι} {f : ι → α}
-    (hs : s.PairwiseDisjoint fun i' : ι' => ⨆ i ∈ g i', f i)
-    (hg : ∀ i ∈ s, (g i).PairwiseDisjoint f) : (⋃ i ∈ s, g i).PairwiseDisjoint f := by
-  rintro a ha b hb hab
-  simp_rw [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
-  -- Porting note: the elaborator couldn't figure out `f` here.
-  · exact (hs hc hd <| ne_of_apply_ne _ hcd).mono
-      (le_supᵢ₂ (f := fun i (_ : i ∈ g c) => f i) a ha)
-      (le_supᵢ₂ (f := fun i (_ : i ∈ g d) => f i) b hb)
-#align set.pairwise_disjoint.bUnion Set.PairwiseDisjoint.bunionᵢ
-
-end CompleteLattice
-
 /-! ### Pairwise disjoint set of sets -/
 
 theorem pairwiseDisjoint_range_singleton :
@@ -415,22 +361,6 @@ theorem PairwiseDisjoint.elim_set {s : Set ι} {f : ι → Set α} (hs : s.Pairw
   hs.elim hi hj <| not_disjoint_iff.2 ⟨a, hai, haj⟩
 #align set.pairwise_disjoint.elim_set Set.PairwiseDisjoint.elim_set
 
-theorem bunionᵢ_diff_bunionᵢ_eq {s t : Set ι} {f : ι → Set α} (h : (s ∪ t).PairwiseDisjoint f) :
-    ((⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i) = ⋃ i ∈ s \ t, f i := by
-  refine'
-    (bunionᵢ_diff_bunionᵢ_subset f s t).antisymm
-      (unionᵢ₂_subset fun 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⟩
-#align set.bUnion_diff_bUnion_eq Set.bunionᵢ_diff_bunionᵢ_eq
-
-/-- Equivalence between a disjoint bounded union and a dependent sum. -/
-noncomputable def bunionᵢEqSigmaOfDisjoint {s : Set ι} {f : ι → Set α} (h : s.PairwiseDisjoint f) :
-    (⋃ i ∈ s, f i) ≃ Σi : s, f i :=
-  (Equiv.setCongr (bunionᵢ_eq_unionᵢ _ _)).trans <|
-    unionEqSigmaOfDisjoint fun ⟨_i, hi⟩ ⟨_j, hj⟩ ne => (h hi hj) fun eq => ne <| Subtype.eq eq
-#align set.bUnion_eq_sigma_of_disjoint Set.bunionᵢEqSigmaOfDisjoint
-
 /-- The partial images of a binary function `f` whose partial evaluations are injective are pairwise
 disjoint iff `f` is injective . -/
 theorem pairwiseDisjoint_image_right_iff {f : α → β → γ} {s : Set α} {t : Set β}
@@ -466,29 +396,3 @@ end Set
 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
-
-section
-
-variable {f : ι → Set α} {s t : Set ι}
-
-theorem Set.PairwiseDisjoint.subset_of_bunionᵢ_subset_bunionᵢ (h₀ : (s ∪ t).PairwiseDisjoint f)
-    (h₁ : ∀ i ∈ s, (f i).Nonempty) (h : (⋃ i ∈ s, f i) ⊆ ⋃ i ∈ t, f i) : s ⊆ t := by
-  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⟩)]
-#align set.pairwise_disjoint.subset_of_bUnion_subset_bUnion Set.PairwiseDisjoint.subset_of_bunionᵢ_subset_bunionᵢ
-
-theorem 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.PairwiseDisjoint.subset_of_bunionᵢ_subset_bunionᵢ (h₀.set_pairwise _) h₁ h
-#align pairwise.subset_of_bUnion_subset_bUnion Pairwise.subset_of_bunionᵢ_subset_bunionᵢ
-
-theorem Pairwise.bunionᵢ_injective (h₀ : Pairwise (Disjoint on f)) (h₁ : ∀ i, (f i).Nonempty) :
-    Injective fun s : Set ι => ⋃ i ∈ s, f i := fun _ _ h =>
-  ((h₀.subset_of_bunionᵢ_subset_bunionᵢ fun _ _ => h₁ _) <| h.subset).antisymm <|
-    (h₀.subset_of_bunionᵢ_subset_bunionᵢ fun _ _ => h₁ _) <| h.superset
-#align pairwise.bUnion_injective Pairwise.bunionᵢ_injective
-
-end