chore(Fintype): move nonempty_fintype (#20053)

This implication doesn't need the axiom of choice or `Fintype.card`.
Currently, it depends on `Classical.choice`
because `Fin.fintype` depends on it (for no good reason).

Author: urkud

Mathlib/Algebra/Order/Field/Pi.lean

@@ -5,7 +5,7 @@ Authors: Yaël Dillies
 -/
 import Mathlib.Algebra.Order.Monoid.Defs
 import Mathlib.Data.Finset.Lattice.Fold
-import Mathlib.Data.Fintype.Card
+import Mathlib.Data.Fintype.Basic
 
 /-!
 # Lemmas about (finite domain) functions into fields.

Mathlib/Data/Finite/Defs.lean

@@ -118,6 +118,10 @@ theorem Function.Bijective.finite_iff {f : α → β} (h : Bijective f) : Finite
 theorem Finite.ofBijective [Finite α] {f : α → β} (h : Bijective f) : Finite β :=
   h.finite_iff.mp ‹_›
 
+variable (α) in
+theorem Finite.nonempty_decidableEq [Finite α] : Nonempty (DecidableEq α) :=
+  let ⟨_n, ⟨e⟩⟩ := Finite.exists_equiv_fin α; ⟨e.decidableEq⟩
+
 instance [Finite α] : Finite (PLift α) :=
   Finite.of_equiv α Equiv.plift.symm
 

Mathlib/Data/Finset/PiInduction.lean

@@ -5,7 +5,7 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Data.Finset.Max
 import Mathlib.Data.Finset.Sigma
-import Mathlib.Data.Fintype.Card
+import Mathlib.Data.Fintype.Basic
 
 /-!
 # Induction principles for `∀ i, Finset (α i)`

Mathlib/Data/Fintype/Basic.lean

@@ -777,6 +777,11 @@ instance Fin.fintype (n : ℕ) : Fintype (Fin n) :=
 theorem Fin.univ_def (n : ℕ) : (univ : Finset (Fin n)) = ⟨List.finRange n, List.nodup_finRange n⟩ :=
   rfl
 
+/-- See also `nonempty_encodable`, `nonempty_denumerable`. -/
+theorem nonempty_fintype (α : Type*) [Finite α] : Nonempty (Fintype α) := by
+  rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩
+  exact ⟨.ofEquiv _ e.symm⟩
+
 @[simp] theorem List.toFinset_finRange (n : ℕ) : (List.finRange n).toFinset = Finset.univ := by
   ext; simp
 

Mathlib/Data/Fintype/Card.lean

@@ -378,14 +378,7 @@ instance (priority := 900) Finite.of_fintype (α : Type*) [Fintype α] : Finite
   Fintype.finite ‹_›
 
 theorem finite_iff_nonempty_fintype (α : Type*) : Finite α ↔ Nonempty (Fintype α) :=
-  ⟨fun h =>
-    let ⟨_k, ⟨e⟩⟩ := @Finite.exists_equiv_fin α h
-    ⟨Fintype.ofEquiv _ e.symm⟩,
-    fun ⟨_⟩ => inferInstance⟩
-
-/-- See also `nonempty_encodable`, `nonempty_denumerable`. -/
-theorem nonempty_fintype (α : Type*) [Finite α] : Nonempty (Fintype α) :=
-  (finite_iff_nonempty_fintype α).mp ‹_›
+  ⟨fun _ => nonempty_fintype α, fun ⟨_⟩ => inferInstance⟩
 
 /-- Noncomputably get a `Fintype` instance from a `Finite` instance. This is not an
 instance because we want `Fintype` instances to be useful for computations. -/

Mathlib/Data/Fintype/Lattice.lean

@@ -3,8 +3,8 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Mathlib.Data.Fintype.Card
 import Mathlib.Data.Finset.Max
+import Mathlib.Data.Fintype.Basic
 
 /-!
 # Lemmas relating fintypes and order/lattice structure.