refactor(data/{finite,fintype}): move some lemmas to `data.fintype.ba…

…sic` (#15626)

We should have lemmas like `nonempty_fintype` in `fintype.basic` to replace `[fintype _]` by `[finite _]` in the assumptions. This PR doesn't fix any assumptions to keep it small.

src/data/finite/basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
 import data.fintype.basic
-import data.finite.defs
 
 /-!
 # Finite types
@@ -43,25 +42,6 @@ open_locale classical
 
 variables {α β γ : Type*}
 
-protected lemma fintype.finite {α : Type*} (h : fintype α) : finite α := ⟨fintype.equiv_fin α⟩
-
-/-- For efficiency reasons, we want `finite` instances to have higher
-priority than ones coming from `fintype` instances. -/
-@[priority 900]
-instance finite.of_fintype (α : Type*) [fintype α] : finite α := fintype.finite ‹_›
-
-lemma finite_iff_nonempty_fintype (α : Type*) :
-  finite α ↔ nonempty (fintype α) :=
-⟨λ h, let ⟨k, ⟨e⟩⟩ := @finite.exists_equiv_fin α h in ⟨fintype.of_equiv _ e.symm⟩,
-  λ ⟨_⟩, by exactI infer_instance⟩
-
-lemma nonempty_fintype (α : Type*) [finite α] : nonempty (fintype α) :=
-(finite_iff_nonempty_fintype α).mp ‹_›
-
-/-- Noncomputably get a `fintype` instance from a `finite` instance. This is not an
-instance because we want `fintype` instances to be useful for computations. -/
-def fintype.of_finite (α : Type*) [finite α] : fintype α := (nonempty_fintype α).some
-
 lemma not_finite_iff_infinite {α : Type*} : ¬ finite α ↔ infinite α :=
 by rw [← is_empty_fintype, finite_iff_nonempty_fintype, not_nonempty_iff]
 
@@ -99,17 +79,6 @@ lemma exists_min [finite α] [nonempty α] [linear_order β] (f : α → β) :
   ∃ x₀ : α, ∀ x, f x₀ ≤ f x :=
 by { haveI := fintype.of_finite α, exact fintype.exists_min f }
 
-lemma of_injective {α β : Sort*} [finite β] (f : α → β) (H : function.injective f) : finite α :=
-begin
-  haveI := fintype.of_finite (plift β),
-  rw [← equiv.injective_comp equiv.plift f, ← equiv.comp_injective _ equiv.plift.symm] at H,
-  haveI := fintype.of_injective _ H,
-  exact finite.of_equiv _ equiv.plift,
-end
-
-lemma of_surjective {α β : Sort*} [finite α] (f : α → β) (H : function.surjective f) : finite β :=
-of_injective _ $ function.injective_surj_inv H
-
 @[priority 100] -- see Note [lower instance priority]
 instance of_is_empty {α : Sort*} [is_empty α] : finite α := finite.of_equiv _ equiv.plift
 

src/data/fintype/basic.lean

@@ -10,6 +10,7 @@ import data.finset.pi
 import data.finset.powerset
 import data.finset.prod
 import data.finset.sigma
+import data.finite.defs
 import data.list.nodup_equiv_fin
 import data.sym.basic
 import data.ulift
@@ -1016,6 +1017,44 @@ rfl
 
 end finset
 
+/-!
+### Relation to `finite`
+
+In this section we prove that `α : Type*` is `finite` if and only if `fintype α` is nonempty.
+-/
+
+@[nolint fintype_finite]
+protected lemma fintype.finite {α : Type*} (h : fintype α) : finite α := ⟨fintype.equiv_fin α⟩
+
+/-- For efficiency reasons, we want `finite` instances to have higher
+priority than ones coming from `fintype` instances. -/
+@[nolint fintype_finite, priority 900]
+instance finite.of_fintype (α : Type*) [fintype α] : finite α := fintype.finite ‹_›
+
+lemma finite_iff_nonempty_fintype (α : Type*) :
+  finite α ↔ nonempty (fintype α) :=
+⟨λ h, let ⟨k, ⟨e⟩⟩ := @finite.exists_equiv_fin α h in ⟨fintype.of_equiv _ e.symm⟩,
+  λ ⟨_⟩, by exactI infer_instance⟩
+
+lemma nonempty_fintype (α : Type*) [finite α] : nonempty (fintype α) :=
+(finite_iff_nonempty_fintype α).mp ‹_›
+
+/-- Noncomputably get a `fintype` instance from a `finite` instance. This is not an
+instance because we want `fintype` instances to be useful for computations. -/
+noncomputable def fintype.of_finite (α : Type*) [finite α] : fintype α := (nonempty_fintype α).some
+
+lemma finite.of_injective {α β : Sort*} [finite β] (f : α → β) (H : injective f) : finite α :=
+begin
+  casesI nonempty_fintype (plift β),
+  rw [← equiv.injective_comp equiv.plift f, ← equiv.comp_injective _ equiv.plift.symm] at H,
+  haveI := fintype.of_injective _ H,
+  exact finite.of_equiv _ equiv.plift,
+end
+
+lemma finite.of_surjective {α β : Sort*} [finite α] (f : α → β) (H : surjective f) :
+  finite β :=
+finite.of_injective _ $ injective_surj_inv H
+
 namespace fintype
 variables [fintype α] [fintype β]