chore(Equiv/Fintype): Fintype -> Finite (#10723)

Mathlib/Logic/Equiv/Fintype.lean

@@ -27,6 +27,7 @@ sides of the equivalence are `Fintype`s.
    computational performance, since it operates by exhaustive search over the input `Fintype`s.
 -/
 
+section Fintype
 
 variable {α β : Type*} [Fintype α] [DecidableEq β] (e : Equiv.Perm α) (f : α ↪ β)
 
@@ -92,15 +93,19 @@ theorem Equiv.Perm.viaFintypeEmbedding_sign [DecidableEq α] [Fintype β] :
   simp [Equiv.Perm.viaFintypeEmbedding]
 #align equiv.perm.via_fintype_embedding_sign Equiv.Perm.viaFintypeEmbedding_sign
 
+end Fintype
+
 namespace Equiv
 
-/-- If `e` is an equivalence between two subtypes of a fintype `α`, `e.toCompl`
+variable {α β : Type*} [Finite α]
+
+/-- If `e` is an equivalence between two subtypes of a finite type `α`, `e.toCompl`
 is an equivalence between the complement of those subtypes.
 
 See also `Equiv.compl`, for a computable version when a term of type
 `{e' : α ≃ α // ∀ x : {x // p x}, e' x = e x}` is known. -/
-noncomputable def toCompl {α : Type*} [Finite α] {p q : α → Prop}
-    (e : { x // p x } ≃ { x // q x }) : { x // ¬p x } ≃ { x // ¬q x } := by
+noncomputable def toCompl {p q : α → Prop} (e : { x // p x } ≃ { x // q x }) :
+    { x // ¬p x } ≃ { x // ¬q x } := by
   apply Classical.choice
   cases nonempty_fintype α
   classical