split(data/finset/*): Split data.finset.card and data.finset.fin …

…off `data.finset.basic` (#10796)

This moves stuff from `data.finset.basic` in two new files:
* Stuff about `finset.card` goes into `data.finset.card`
* Stuff about `finset.fin_range` and `finset.attach_fin` goes into `data.finset.fin`. I expect this file to be shortlived as I'm planning on killing `fin_range`.

I reordered lemmas thematically and it appeared that there were two pairs of duplicated lemmas:
* `finset.one_lt_card`, `finset.one_lt_card_iff`. They differ only for binder order.
* `finset.card_union_eq`, `finset.card_disjoint_union`. They are literally the same.

All are used so I will clean up in a later PR.

I'm crediting:
* Microsoft Corporation, Leonardo, Jeremy for 8dbee5b
* Chris Hughes for #231
* Scott for #3319

src/combinatorics/set_family/compression/uv.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
-import data.finset.basic
+import data.finset.card
 
 /-!
 # UV-compressions

src/data/finset/fin.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2018 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes, Scott Morrison, Johan Commelin
+-/
+import data.finset.card
+
+/-!
+# Finsets in `fin n`
+
+A few constructions for finsets in `fin n`.
+
+## Main declarations
+
+* `finset.fin_range`: `{0, 1, ..., n - 1}` as a `finset (fin n)`.
+* `finset.attach_fin`: Turns a finset of naturals strictly less than `n` into a `finset (fin n)`.
+-/
+
+variables {n : ℕ}
+
+namespace finset
+
+/-- `finset.fin_range n` is the finset `{0, 1, ..., n - 1}`, as a `finset (fin n)`. -/
+def fin_range (n : ℕ) : finset (fin n) := ⟨list.fin_range n, list.nodup_fin_range n⟩
+
+@[simp]
+lemma fin_range_card : (fin_range n).card = n := by simp [fin_range]
+
+@[simp]
+lemma mem_fin_range (m : fin n) : m ∈ fin_range n := list.mem_fin_range m
+
+@[simp] lemma coe_fin_range (n : ℕ) : (fin_range n : set (fin n)) = set.univ :=
+set.eq_univ_of_forall mem_fin_range
+
+/-- Given a finset `s` of `ℕ` contained in `{0,..., n-1}`, the corresponding finset in `fin n`
+is `s.attach_fin h` where `h` is a proof that all elements of `s` are less than `n`. -/
+def attach_fin (s : finset ℕ) {n : ℕ} (h : ∀ m ∈ s, m < n) : finset (fin n) :=
+⟨s.1.pmap (λ a ha, ⟨a, ha⟩) h, multiset.nodup_pmap (λ _ _ _ _, fin.veq_of_eq) s.2⟩
+
+@[simp] lemma mem_attach_fin {n : ℕ} {s : finset ℕ} (h : ∀ m ∈ s, m < n) {a : fin n} :
+  a ∈ s.attach_fin h ↔ (a : ℕ) ∈ s :=
+⟨λ h, let ⟨b, hb₁, hb₂⟩ := multiset.mem_pmap.1 h in hb₂ ▸ hb₁,
+λ h, multiset.mem_pmap.2 ⟨a, h, fin.eta _ _⟩⟩
+
+@[simp] lemma card_attach_fin {n : ℕ} (s : finset ℕ) (h : ∀ m ∈ s, m < n) :
+  (s.attach_fin h).card = s.card :=
+multiset.card_pmap _ _ _
+
+end finset

src/data/finset/nat_antidiagonal.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
-import data.finset.basic
+import data.finset.card
 import data.multiset.nat_antidiagonal
 
 /-!

src/data/finset/option.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Mario Carneiro, Sean Leather
 -/
-import data.finset.basic
+import data.finset.card
 import order.hom.basic
 
 /-!

src/data/finset/prod.lean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Oliver Nash
 -/
-import data.finset.basic
+import data.finset.card
 
 /-!
 # Finsets in product types

src/data/fintype/basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import data.array.lemmas
+import data.finset.fin
 import data.finset.option
 import data.finset.pi
 import data.finset.powerset

src/group_theory/perm/support.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Aaron Anderson, Yakov Pechersky
 -/
+import data.finset.card
 import data.fintype.basic
 import group_theory.perm.basic