split(data/finset/sigma): Split off data.finset.basic (#10957)

This moves `finset.sigma` to a new file `data.finset.sigma`.

I'm crediting Mario for 16d40d7

Author: YaelDillies

src/data/finset/basic.lean

@@ -101,7 +101,6 @@ called `top` with `⊤ = univ`.
 * `finset.sdiff`: Defines the set difference `s \ t` for finsets `s` and `t`.
 * `finset.product`: Given finsets of `α` and `β`, defines finsets of `α × β`.
   For arbitrary dependent products, see `data.finset.pi`.
-* `finset.sigma`: Given finsets of `α` and `β`, defines finsets of the dependent sum type `Σ α, β`
 * `finset.bUnion`: Finite unions of finsets; given an indexing function `f : α → finset β` and a
   `s : finset α`, `s.bUnion f` is the union of all finsets of the form `f a` for `a ∈ s`.
 * `finset.bInter`: TODO: Implemement finite intersections.
@@ -2435,33 +2434,6 @@ bUnion_nonempty.2 $ hs.imp $ λ x hx, ⟨hx, ht x hx⟩
 
 end bUnion
 
-/-! ### sigma -/
-section sigma
-variables {σ : α → Type*} {s : finset α} {t : Πa, finset (σ a)}
-
-/-- `sigma s t` is the set of dependent pairs `⟨a, b⟩` such that `a ∈ s` and `b ∈ t a`. -/
-protected def sigma (s : finset α) (t : Πa, finset (σ a)) : finset (Σa, σ a) :=
-⟨_, nodup_sigma s.2 (λ a, (t a).2)⟩
-
-@[simp] theorem mem_sigma {p : sigma σ} : p ∈ s.sigma t ↔ p.1 ∈ s ∧ p.2 ∈ t (p.1) := mem_sigma
-
-@[simp] theorem sigma_nonempty : (s.sigma t).nonempty ↔ ∃ x ∈ s, (t x).nonempty :=
-by simp [finset.nonempty]
-
-@[simp] theorem sigma_eq_empty : s.sigma t = ∅ ↔ ∀ x ∈ s, t x = ∅ :=
-by simp only [← not_nonempty_iff_eq_empty, sigma_nonempty, not_exists]
-
-@[mono] theorem sigma_mono {s₁ s₂ : finset α} {t₁ t₂ : Πa, finset (σ a)}
-  (H1 : s₁ ⊆ s₂) (H2 : ∀a, t₁ a ⊆ t₂ a) : s₁.sigma t₁ ⊆ s₂.sigma t₂ :=
-λ ⟨x, sx⟩ H, let ⟨H3, H4⟩ := mem_sigma.1 H in mem_sigma.2 ⟨H1 H3, H2 x H4⟩
-
-theorem sigma_eq_bUnion [decidable_eq (Σ a, σ a)] (s : finset α)
-  (t : Πa, finset (σ a)) :
-  s.sigma t = s.bUnion (λa, (t a).map $ embedding.sigma_mk a) :=
-by { ext ⟨x, y⟩, simp [and.left_comm] }
-
-end sigma
-
 /-! ### disjoint -/
 section disjoint
 variable [decidable_eq α]

src/data/finset/lattice.lean

@@ -118,17 +118,6 @@ end
 @[simp] lemma sup_attach (s : finset β) (f : β → α) : s.attach.sup (λ x, f x) = s.sup f :=
 (s.attach.sup_map (function.embedding.subtype _) f).symm.trans $ congr_arg _ attach_map_val
 
-lemma sup_sigma {γ : β → Type*} (s : finset β) (t : Π i, finset (γ i)) (f : sigma γ → α) :
-  (s.sigma t).sup f = s.sup (λ i, (t i).sup $ λ b, f ⟨i, b⟩) :=
-begin
-  refine le_antisymm _ (sup_le (λ i hi, sup_le $ λ b hb, le_sup $ mem_sigma.2 ⟨hi, hb⟩)),
-  refine sup_le _,
-  rintro ⟨i, b⟩ hb,
-  rw mem_sigma at hb,
-  refine le_trans _ (le_sup hb.1),
-  convert le_sup hb.2,
-end
-
 /-- See also `finset.product_bUnion`. -/
 lemma sup_product_left (s : finset β) (t : finset γ) (f : β × γ → α) :
   (s.product t).sup f = s.sup (λ i, t.sup $ λ i', f ⟨i, i'⟩) :=
@@ -341,10 +330,6 @@ lemma inf_comm (s : finset β) (t : finset γ) (f : β → γ → α) :
   s.inf (λ b, t.inf (f b)) = t.inf (λ c, s.inf (λ b, f b c)) :=
 @sup_comm (order_dual α) _ _ _ _ _ _ _
 
-lemma inf_sigma {γ : β → Type*} (s : finset β) (t : Π i, finset (γ i)) (f : sigma γ → α) :
-  (s.sigma t).inf f = s.inf (λ i, (t i).inf $ λ b, f ⟨i, b⟩) :=
-@sup_sigma (order_dual α) _ _ _ _ _ _ _
-
 lemma inf_product_left (s : finset β) (t : finset γ) (f : β × γ → α) :
   (s.product t).inf f = s.inf (λ i, t.inf $ λ i', f ⟨i, i'⟩) :=
 @sup_product_left (order_dual α) _ _ _ _ _ _ _

src/data/finset/sigma.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import data.finset.lattice
+
+/-!
+# Finite sets in a sigma type
+
+This file defines a `finset` construction on `Σ i, α i`.
+
+## Main declarations
+
+* `finset.sigma`: Given a finset `s` in `ι` and finsets `t i` in each `α i`, `s.sigma t` is the
+  finset of the dependent sum `Σ i, α i`
+-/
+
+open function multiset
+
+namespace finset
+variables {ι β : Type*} {α : ι → Type*} (s s₁ s₂ : finset ι) (t t₁ t₂ : Π i, finset (α i))
+
+/-- `s.sigma t` is the finset of dependent pairs `⟨i, a⟩` such that `i ∈ s` and `a ∈ t i`. -/
+protected def sigma : finset (Σ i, α i) := ⟨_, nodup_sigma s.2 (λ i, (t i).2)⟩
+
+variables {s s₁ s₂ t t₁ t₂}
+
+@[simp] lemma mem_sigma {a : Σ i, α i} : a ∈ s.sigma t ↔ a.1 ∈ s ∧ a.2 ∈ t a.1 := mem_sigma
+
+@[simp] lemma sigma_nonempty : (s.sigma t).nonempty ↔ ∃ i ∈ s, (t i).nonempty :=
+by simp [finset.nonempty]
+
+@[simp] lemma sigma_eq_empty : s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅ :=
+by simp only [← not_nonempty_iff_eq_empty, sigma_nonempty, not_exists]
+
+@[mono] lemma sigma_mono (hs : s₁ ⊆ s₂) (ht : ∀ i, t₁ i ⊆ t₂ i) : s₁.sigma t₁ ⊆ s₂.sigma t₂ :=
+λ ⟨i, a⟩ h, let ⟨hi, ha⟩ := mem_sigma.1 h in mem_sigma.2 ⟨hs hi, ht i ha⟩
+
+lemma sigma_eq_bUnion [decidable_eq (Σ i, α i)] (s : finset ι) (t : Π i, finset (α i)) :
+  s.sigma t = s.bUnion (λ i, (t i).map $ embedding.sigma_mk i) :=
+by { ext ⟨x, y⟩, simp [and.left_comm] }
+
+variables (s t) (f : (Σ i, α i) → β)
+
+lemma sup_sigma [semilattice_sup β] [order_bot β] :
+  (s.sigma t).sup f = s.sup (λ i, (t i).sup $ λ b, f ⟨i, b⟩) :=
+begin
+  refine (sup_le _).antisymm (sup_le $ λ i hi, sup_le $ λ b hb, le_sup $ mem_sigma.2 ⟨hi, hb⟩),
+  rintro ⟨i, b⟩ hb,
+  rw mem_sigma at hb,
+  refine le_trans _ (le_sup hb.1),
+  convert le_sup hb.2,
+end
+
+lemma inf_sigma [semilattice_inf β] [order_top β] :
+  (s.sigma t).inf f = s.inf (λ i, (t i).inf $ λ b, f ⟨i, b⟩) :=
+@sup_sigma _ (order_dual β) _ _ _ _ _ _
+
+end finset

src/data/fintype/basic.lean

@@ -9,6 +9,7 @@ import data.finset.option
 import data.finset.pi
 import data.finset.powerset
 import data.finset.prod
+import data.finset.sigma
 import data.list.nodup_equiv_fin
 import data.sym.basic
 import data.ulift