chore(data/fintype/basic): split, and reduce imports (#3319)

Following on from #3256 and #3235, this slices a little out of `data.fintype.basic`, and reduces imports, mostly in the vicinity of `data.fintype.basic`.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/combinatorics/composition.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import data.fintype.card
-import tactic.omega
+import data.finset.sort
 
 /-!
 # Compositions

src/control/bifunctor.lean

@@ -6,7 +6,8 @@ Author: Simon Hudon
 Functors with two arguments
 -/
 import logic.function.basic
-import tactic.basic
+import control.functor
+import tactic.core
 
 universes u₀ u₁ u₂ v₀ v₁ v₂
 

src/control/bitraversable/basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Simon Hudon
 -/
 import control.bifunctor
+import control.traversable.basic
 
 /-!
 # Bitraversable type class

src/control/bitraversable/instances.lean

@@ -76,7 +76,7 @@ instance bitraversable.flip : bitraversable (flip t) :=
 open is_lawful_bitraversable
 instance is_lawful_bitraversable.flip [is_lawful_bitraversable t]
   : is_lawful_bitraversable (flip t)  :=
-by constructor; intros; unfreezingI { casesm is_lawful_bitraversable t }; apply_assumption
+by constructor; intros; unfreezingI { casesm is_lawful_bitraversable t }; tactic.apply_assumption
 
 open bitraversable functor
 

src/data/equiv/list.lean

@@ -6,6 +6,7 @@ Author: Mario Carneiro
 Additional equiv and encodable instances for lists, finsets, and fintypes.
 -/
 import data.equiv.denumerable
+import data.finset.sort
 
 open nat list
 

src/data/finset/basic.lean

@@ -1940,6 +1940,18 @@ lemma exists_smaller_set (A : finset α) (i : ℕ) (h₁ : i ≤ card A) :
   ∃ (B : finset α), B ⊆ A ∧ card B = i :=
 let ⟨B, _, x₁, x₂⟩ := exists_intermediate_set i (by simpa) (empty_subset A) in ⟨B, x₁, x₂⟩
 
+/-- `finset.fin_range k` is the finset `{0, 1, ..., k-1}`, as a `finset (fin k)`. -/
+def fin_range (k : ℕ) : finset (fin k) :=
+⟨list.fin_range k, list.nodup_fin_range k⟩
+
+@[simp]
+lemma fin_range_card {k : ℕ} : (fin_range k).card = k :=
+by simp [fin_range]
+
+@[simp]
+lemma mem_fin_range {k : ℕ} (m : fin k) : m ∈ fin_range k :=
+list.mem_fin_range m
+
 /-- 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) :=

src/data/finset/sort.lean

@@ -5,6 +5,7 @@ Author: Mario Carneiro
 -/
 import data.finset.lattice
 import data.multiset.sort
+import tactic.suggest
 
 /-!
 # Construct a sorted list from a finset.
@@ -90,6 +91,7 @@ def mono_of_fin (s : finset α) {k : ℕ} (h : s.card = k) (i : fin k) : α :=
 have A : (i : ℕ) < (s.sort (≤)).length, by simpa [h] using i.2,
 (s.sort (≤)).nth_le i A
 
+
 lemma mono_of_fin_strict_mono (s : finset α) {k : ℕ} (h : s.card = k) :
   strict_mono (s.mono_of_fin h) :=
 begin
@@ -175,6 +177,21 @@ begin
     exact (ne_of_lt (mono_of_fin_strict_mono s h ji) hj).elim }
 end
 
+/-- Any increasing map between `fin k` and a finset of cardinality `k` has to coincide with
+the increasing bijection `mono_of_fin s h`. -/
+lemma mono_of_fin_unique' {s : finset α} {k : ℕ} (h : s.card = k)
+  {f : fin k → α} (fmap : set.maps_to f set.univ ↑s) (hmono : strict_mono f) :
+  f = s.mono_of_fin h :=
+begin
+  have finj : set.inj_on f set.univ := hmono.injective.inj_on _,
+  apply mono_of_fin_unique h (set.bij_on.mk fmap finj (λ y hy, _)) hmono,
+  simp only [set.image_univ, set.mem_range],
+  rcases surj_on_of_inj_on_of_card_le (λ i (hi : i ∈ finset.fin_range k), f i)
+    (λ i hi, fmap (set.mem_univ i)) (λ i j hi hj hij, finj (set.mem_univ i) (set.mem_univ j) hij)
+    (by simp [h]) y hy with ⟨x, _, hx⟩,
+  exact ⟨x, hx.symm⟩
+end
+
 /-- Two parametrizations `mono_of_fin` of the same set take the same value on `i` and `j` if and
 only if `i = j`. Since they can be defined on a priori not defeq types `fin k` and `fin l` (although
 necessarily `k = l`), the conclusion is rather written `i.val = j.val`. -/

src/data/fintype/basic.lean

@@ -5,8 +5,8 @@ Author: Mario Carneiro
 
 Finite types.
 -/
-import data.finset.sort
 import data.finset.powerset
+import data.finset.lattice
 import data.finset.pi
 import data.array.lemmas
 
@@ -144,18 +144,6 @@ quot.rec_on_subsingleton (@univ α _).1
 theorem exists_equiv_fin (α) [fintype α] : ∃ n, nonempty (α ≃ fin n) :=
 by haveI := classical.dec_eq α; exact ⟨card α, nonempty_of_trunc (equiv_fin α)⟩
 
-/-- Given a linearly ordered fintype `α` of cardinal `k`, the equiv `mono_equiv_of_fin α h`
-is the increasing bijection between `fin k` and `α`. Here, `h` is a proof that
-the cardinality of `s` is `k`. We use this instead of a map `fin s.card → α` to avoid
-casting issues in further uses of this function. -/
-noncomputable def mono_equiv_of_fin (α) [fintype α] [decidable_linear_order α] {k : ℕ}
-  (h : fintype.card α = k) : fin k ≃ α :=
-equiv.of_bijective (mono_of_fin univ h) begin
-  apply set.bijective_iff_bij_on_univ.2,
-  rw ← @coe_univ α _,
-  exact mono_of_fin_bij_on (univ : finset α) h
-end
-
 instance (α : Type*) : subsingleton (fintype α) :=
 ⟨λ ⟨s₁, h₁⟩ ⟨s₂, h₂⟩, by congr; simp [finset.ext_iff, h₁, h₂]⟩
 
@@ -266,7 +254,7 @@ lemma finset.card_univ_diff [fintype α] [decidable_eq α] (s : finset α) :
 finset.card_sdiff (subset_univ s)
 
 instance (n : ℕ) : fintype (fin n) :=
-⟨⟨list.fin_range n, list.nodup_fin_range n⟩, list.mem_fin_range⟩
+⟨finset.fin_range n, finset.mem_fin_range⟩
 
 @[simp] theorem fintype.card_fin (n : ℕ) : fintype.card (fin n) = n :=
 list.length_fin_range n
@@ -295,21 +283,6 @@ begin
     exact fin.eq_last_of_not_lt h }
 end
 
-/-- Any increasing map between `fin k` and a finset of cardinality `k` has to coincide with
-the increasing bijection `mono_of_fin s h`. -/
-lemma finset.mono_of_fin_unique' [decidable_linear_order α] {s : finset α} {k : ℕ} (h : s.card = k)
-  {f : fin k → α} (fmap : set.maps_to f set.univ ↑s) (hmono : strict_mono f) :
-  f = s.mono_of_fin h :=
-begin
-  have finj : set.inj_on f set.univ := hmono.injective.inj_on _,
-  apply mono_of_fin_unique h (set.bij_on.mk fmap finj (λ y hy, _)) hmono,
-  simp only [set.image_univ, set.mem_range],
-  rcases surj_on_of_inj_on_of_card_le (λ i (hi : i ∈ finset.univ), f i)
-    (λ i hi, fmap (set.mem_univ i)) (λ i j hi hj hij, finj (set.mem_univ i) (set.mem_univ j) hij)
-    (by simp [h]) y hy with ⟨x, _, hx⟩,
-  exact ⟨x, hx.symm⟩
-end
-
 @[instance, priority 10] def unique.fintype {α : Type*} [unique α] : fintype α :=
 fintype.of_subsingleton (default α)
 

src/data/fintype/sort.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Mario Carneiro
+-/
+import data.fintype.basic
+import data.finset.sort
+
+variables {α : Type*}
+
+open finset
+
+/-- Given a linearly ordered fintype `α` of cardinal `k`, the equiv `mono_equiv_of_fin α h`
+is the increasing bijection between `fin k` and `α`. Here, `h` is a proof that
+the cardinality of `s` is `k`. We use this instead of a map `fin s.card → α` to avoid
+casting issues in further uses of this function. -/
+noncomputable def mono_equiv_of_fin (α) [fintype α] [decidable_linear_order α] {k : ℕ}
+  (h : fintype.card α = k) : fin k ≃ α :=
+equiv.of_bijective (mono_of_fin univ h) begin
+  apply set.bijective_iff_bij_on_univ.2,
+  rw ← @coe_univ α _,
+  exact mono_of_fin_bij_on (univ : finset α) h
+end

src/data/polynomial.lean

@@ -11,6 +11,7 @@ import algebra.gcd_domain
 import ring_theory.euclidean_domain
 import ring_theory.multiplicity
 import data.finset.nat_antidiagonal
+import data.finset.sort
 
 /-!
 # Theory of univariate polynomials