chore: move Fin material earlier (#19186)

This will in particular be used in #19086 to prove `Finite Bool` and `Finite Prop` much earlier.

Mathlib/Algebra/Ring/Fin.lean

@@ -5,7 +5,7 @@ Authors: Anne Baanen
 -/
 import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.Ring.Equiv
-import Mathlib.Logic.Equiv.Fin
+import Mathlib.Data.Fin.Tuple.Basic
 
 /-!
 # Rings and `Fin`

Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean

@@ -7,7 +7,6 @@ import Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
 import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
 import Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
-import Mathlib.Logic.Equiv.Fin
 
 /-!
 # Constructing finite products from binary products and terminal.

Mathlib/CategoryTheory/Monoidal/Types/Basic.lean

@@ -6,7 +6,6 @@ Authors: Michael Jendrusch, Kim Morrison
 import Mathlib.CategoryTheory.Monoidal.Functor
 import Mathlib.CategoryTheory.ChosenFiniteProducts
 import Mathlib.CategoryTheory.Limits.Shapes.Types
-import Mathlib.Logic.Equiv.Fin
 
 /-!
 # The category of types is a monoidal category

Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean

@@ -5,7 +5,6 @@ Authors: Iván Renison
 -/
 import Mathlib.Combinatorics.SimpleGraph.Coloring
 import Mathlib.Combinatorics.SimpleGraph.Hasse
-import Mathlib.Logic.Equiv.Fin
 
 /-!
 # Concrete colorings of common graphs

Mathlib/Data/Countable/Basic.lean

@@ -3,9 +3,9 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Logic.Equiv.Nat
-import Mathlib.Logic.Equiv.Fin
 import Mathlib.Data.Countable.Defs
+import Mathlib.Data.Fin.Tuple.Basic
+import Mathlib.Logic.Equiv.Nat
 
 /-!
 # Countable types

Mathlib/Data/Fin/Basic.lean

@@ -1465,9 +1465,6 @@ protected theorem coe_neg (a : Fin n) : ((-a : Fin n) : ℕ) = (n - a) % n :=
 
 theorem eq_zero (n : Fin 1) : n = 0 := Subsingleton.elim _ _
 
-instance uniqueFinOne : Unique (Fin 1) where
-  uniq _ := Subsingleton.elim _ _
-
 @[deprecated val_eq_zero (since := "2024-09-18")]
 theorem coe_fin_one (a : Fin 1) : (a : ℕ) = 0 := by simp [Subsingleton.elim a 0]
 

Mathlib/Data/Fin/Tuple/Basic.lean

@@ -177,6 +177,18 @@ theorem cons_self_tail : cons (q 0) (tail q) = q := by
     unfold tail
     rw [cons_succ]
 
+/-- Equivalence between tuples of length `n + 1` and pairs of an element and a tuple of length `n`
+given by separating out the first element of the tuple.
+
+This is `Fin.cons` as an `Equiv`. -/
+@[simps]
+def consEquiv (α : Fin (n + 1) → Type*) : α 0 × (∀ i, α (succ i)) ≃ ∀ i, α i where
+  toFun f := cons f.1 f.2
+  invFun f := (f 0, tail f)
+  left_inv f := by simp
+  right_inv f := by simp
+
+
 -- Porting note: Mathport removes `_root_`?
 /-- Recurse on an `n+1`-tuple by splitting it into a single element and an `n`-tuple. -/
 @[elab_as_elim]
@@ -693,6 +705,17 @@ theorem comp_init {α : Sort*} {β : Sort*} (g : α → β) (q : Fin n.succ →
   ext j
   simp [init]
 
+/-- Equivalence between tuples of length `n + 1` and pairs of an element and a tuple of length `n`
+given by separating out the last element of the tuple.
+
+This is `Fin.snoc` as an `Equiv`. -/
+@[simps]
+def snocEquiv (α : Fin (n + 1) → Type*) : α (last n) × (∀ i, α (castSucc i)) ≃ ∀ i, α i where
+  toFun f _ := Fin.snoc f.2 f.1 _
+  invFun f := ⟨f _, Fin.init f⟩
+  left_inv f := by simp
+  right_inv f := by simp
+
 /-- Recurse on an `n+1`-tuple by splitting it its initial `n`-tuple and its last element. -/
 @[elab_as_elim, inline]
 def snocCases {P : (∀ i : Fin n.succ, α i) → Sort*}
@@ -926,6 +949,26 @@ open Set
 lemma insertNth_self_removeNth (p : Fin (n + 1)) (f : ∀ j, α j) :
     insertNth p (f p) (removeNth p f) = f := by simp
 
+/-- Equivalence between tuples of length `n + 1` and pairs of an element and a tuple of length `n`
+given by separating out the `p`-th element of the tuple.
+
+This is `Fin.insertNth` as an `Equiv`. -/
+@[simps]
+def insertNthEquiv (α : Fin (n + 1) → Type u) (p : Fin (n + 1)) :
+    α p × (∀ i, α (p.succAbove i)) ≃ ∀ i, α i where
+  toFun f := insertNth p f.1 f.2
+  invFun f := (f p, removeNth p f)
+  left_inv f := by ext <;> simp
+  right_inv f := by simp
+
+@[simp] lemma insertNthEquiv_zero (α : Fin (n + 1) → Type*) : insertNthEquiv α 0 = consEquiv α :=
+  Equiv.symm_bijective.injective <| by ext <;> rfl
+
+/-- Note this lemma can only be written about non-dependent tuples as `insertNth (last n) = snoc` is
+not a definitional equality. -/
+@[simp] lemma insertNthEquiv_last (n : ℕ) (α : Type*) :
+    insertNthEquiv (fun _ ↦ α) (last n) = snocEquiv (fun _ ↦ α) := by ext; simp
+
 /-- Separates an `n+1`-tuple, returning a selected index and then the rest of the tuple.
 Functional form of `Equiv.piFinSuccAbove`. -/
 @[deprecated removeNth (since := "2024-06-19")]
@@ -1090,3 +1133,12 @@ theorem sigma_eq_iff_eq_comp_cast {α : Type*} {a b : Σii, Fin ii → α} :
     sigma_eq_of_eq_comp_cast _ h'⟩
 
 end Fin
+
+/-- `Π i : Fin 2, α i` is equivalent to `α 0 × α 1`. See also `finTwoArrowEquiv` for a
+non-dependent version and `prodEquivPiFinTwo` for a version with inputs `α β : Type u`. -/
+@[simps (config := .asFn)]
+def piFinTwoEquiv (α : Fin 2 → Type u) : (∀ i, α i) ≃ α 0 × α 1 where
+  toFun f := (f 0, f 1)
+  invFun p := Fin.cons p.1 <| Fin.cons p.2 finZeroElim
+  left_inv _ := funext <| Fin.forall_fin_two.2 ⟨rfl, rfl⟩
+  right_inv := fun _ => rfl

Mathlib/Data/Fin/Tuple/Finset.lean

@@ -5,7 +5,6 @@ Authors: Bolton Bailey
 -/
 import Mathlib.Data.Finset.Prod
 import Mathlib.Data.Fintype.Pi
-import Mathlib.Logic.Equiv.Fin
 
 /-!
 # Fin-indexed tuples of finsets

Mathlib/Data/ZMod/Defs.lean

@@ -101,7 +101,7 @@ instance ZMod.repr : ∀ n : ℕ, Repr (ZMod n)
 
 namespace ZMod
 
-instance instUnique : Unique (ZMod 1) := Fin.uniqueFinOne
+instance instUnique : Unique (ZMod 1) := Fin.instUnique
 
 instance fintype : ∀ (n : ℕ) [NeZero n], Fintype (ZMod n)
   | 0, h => (h.ne _ rfl).elim

Mathlib/Logic/Equiv/Defs.lean

@@ -854,3 +854,22 @@ protected def congrRight {r r' : Setoid α}
   Quot.congrRight eq
 
 end Quotient
+
+/-- Equivalence between `Fin 0` and `Empty`. -/
+def finZeroEquiv : Fin 0 ≃ Empty := .equivEmpty _
+
+/-- Equivalence between `Fin 0` and `PEmpty`. -/
+def finZeroEquiv' : Fin 0 ≃ PEmpty.{u} := .equivPEmpty _
+
+/-- Equivalence between `Fin 1` and `Unit`. -/
+def finOneEquiv : Fin 1 ≃ Unit := .equivPUnit _
+
+/-- Equivalence between `Fin 2` and `Bool`. -/
+def finTwoEquiv : Fin 2 ≃ Bool where
+  toFun i := i == 1
+  invFun b := bif b then 1 else 0
+  left_inv i :=
+    match i with
+    | 0 => by simp
+    | 1 => by simp
+  right_inv b := by cases b <;> simp

Mathlib/Logic/Equiv/Fin.lean

@@ -18,87 +18,6 @@ universe u
 
 variable {m n : ℕ}
 
-/-- Equivalence between `Fin 0` and `Empty`. -/
-def finZeroEquiv : Fin 0 ≃ Empty :=
-  Equiv.equivEmpty _
-
-/-- Equivalence between `Fin 0` and `PEmpty`. -/
-def finZeroEquiv' : Fin 0 ≃ PEmpty.{u} :=
-  Equiv.equivPEmpty _
-
-/-- Equivalence between `Fin 1` and `Unit`. -/
-def finOneEquiv : Fin 1 ≃ Unit :=
-  Equiv.equivPUnit _
-
-/-- Equivalence between `Fin 2` and `Bool`. -/
-def finTwoEquiv : Fin 2 ≃ Bool where
-  toFun := ![false, true]
-  invFun b := b.casesOn 0 1
-  left_inv := Fin.forall_fin_two.2 <| by simp
-  right_inv := Bool.forall_bool.2 <| by simp
-
-/-!
-### Tuples
-
-This section defines a bunch of equivalences between `n + 1`-tuples and products of `n`-tuples with
-an entry.
--/
-
-namespace Fin
-
-/-- Equivalence between tuples of length `n + 1` and pairs of an element and a tuple of length `n`
-given by separating out the first element of the tuple.
-
-This is `Fin.cons` as an `Equiv`. -/
-@[simps]
-def consEquiv (α : Fin (n + 1) → Type*) : α 0 × (∀ i, α (succ i)) ≃ ∀ i, α i where
-  toFun f := cons f.1 f.2
-  invFun f := (f 0, tail f)
-  left_inv f := by simp
-  right_inv f := by simp
-
-/-- Equivalence between tuples of length `n + 1` and pairs of an element and a tuple of length `n`
-given by separating out the last element of the tuple.
-
-This is `Fin.snoc` as an `Equiv`. -/
-@[simps]
-def snocEquiv (α : Fin (n + 1) → Type*) : α (last n) × (∀ i, α (castSucc i)) ≃ ∀ i, α i where
-  toFun f _ := Fin.snoc f.2 f.1 _
-  invFun f := ⟨f _, Fin.init f⟩
-  left_inv f := by simp
-  right_inv f := by simp
-
-/-- Equivalence between tuples of length `n + 1` and pairs of an element and a tuple of length `n`
-given by separating out the `p`-th element of the tuple.
-
-This is `Fin.insertNth` as an `Equiv`. -/
-@[simps]
-def insertNthEquiv (α : Fin (n + 1) → Type u) (p : Fin (n + 1)) :
-    α p × (∀ i, α (p.succAbove i)) ≃ ∀ i, α i where
-  toFun f := insertNth p f.1 f.2
-  invFun f := (f p, removeNth p f)
-  left_inv f := by ext <;> simp
-  right_inv f := by simp
-
-@[simp] lemma insertNthEquiv_zero (α : Fin (n + 1) → Type*) : insertNthEquiv α 0 = consEquiv α :=
-  Equiv.symm_bijective.injective <| by ext <;> rfl
-
-/-- Note this lemma can only be written about non-dependent tuples as `insertNth (last n) = snoc` is
-not a definitional equality. -/
-@[simp] lemma insertNthEquiv_last (n : ℕ) (α : Type*) :
-    insertNthEquiv (fun _ ↦ α) (last n) = snocEquiv (fun _ ↦ α) := by ext; simp
-
-end Fin
-
-/-- `Π i : Fin 2, α i` is equivalent to `α 0 × α 1`. See also `finTwoArrowEquiv` for a
-non-dependent version and `prodEquivPiFinTwo` for a version with inputs `α β : Type u`. -/
-@[simps (config := .asFn)]
-def piFinTwoEquiv (α : Fin 2 → Type u) : (∀ i, α i) ≃ α 0 × α 1 where
-  toFun f := (f 0, f 1)
-  invFun p := Fin.cons p.1 <| Fin.cons p.2 finZeroElim
-  left_inv _ := funext <| Fin.forall_fin_two.2 ⟨rfl, rfl⟩
-  right_inv := fun _ => rfl
-
 /-!
 ### Miscellaneous
 

Mathlib/Logic/Unique.lean

@@ -261,3 +261,5 @@ instance Unique.subtypeEq' (y : α) : Unique { x // y = x } where
   uniq := fun ⟨x, hx⟩ ↦ by subst hx; congr
 
 end Subtype
+
+instance Fin.instUnique : Unique (Fin 1) where uniq _ := Subsingleton.elim _ _

Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

@@ -8,7 +8,6 @@ import Mathlib.Data.Int.Cast.Lemmas
 import Mathlib.Data.Prod.TProd
 import Mathlib.Data.Set.UnionLift
 import Mathlib.GroupTheory.Coset.Defs
-import Mathlib.Logic.Equiv.Fin
 import Mathlib.MeasureTheory.MeasurableSpace.Instances
 import Mathlib.Order.Filter.SmallSets
 import Mathlib.Tactic.FinCases

Mathlib/SetTheory/Cardinal/Basic.lean

@@ -8,6 +8,7 @@ import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Data.Fintype.Powerset
 import Mathlib.Data.Nat.Cast.Order.Basic
 import Mathlib.Data.Set.Countable
+import Mathlib.Logic.Equiv.Fin
 import Mathlib.Logic.Small.Set
 import Mathlib.Logic.UnivLE
 import Mathlib.Order.ConditionallyCompleteLattice.Indexed