chore(CategoryTheory/Limits): Fintype -> Finite (#10915)

Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

@@ -36,9 +36,12 @@ such that `ι j ≫ π j'` is the identity when `j = j'` and zero otherwise.
 As `⊕` is already taken for the sum of types, we introduce the notation `X ⊞ Y` for
 a binary biproduct. We introduce `⨁ f` for the indexed biproduct.
 
-## Implementation
-Prior to #14046, `HasFiniteBiproducts` required a `DecidableEq` instance on the indexing type.
-As this had no pay-off (everything about limits is non-constructive in mathlib), and occasional cost
+## Implementation notes
+
+Prior to leanprover-community/mathlib#14046,
+`HasFiniteBiproducts` required a `DecidableEq` instance on the indexing type.
+As this had no pay-off (everything about limits is non-constructive in mathlib),
+ and occasional cost
 (constructing decidability instances appropriate for constructions involving the indexing type),
 we made everything classical.
 -/
@@ -901,8 +904,8 @@ section
 
 open Classical
 
--- Per #15067, we only allow indexing in `Type 0` here.
-variable {K : Type} [Fintype K] [HasFiniteBiproducts C] (f : K → C)
+-- Per leanprover-community/mathlib#15067, we only allow indexing in `Type 0` here.
+variable {K : Type} [Finite K] [HasFiniteBiproducts C] (f : K → C)
 
 /-- The limit cone exhibiting `⨁ Subtype.restrict pᶜ f` as the kernel of
 `biproduct.toSubtype f p` -/
@@ -988,7 +991,7 @@ namespace Limits
 
 section FiniteBiproducts
 
-variable {J : Type} [Fintype J] {K : Type} [Fintype K] {C : Type u} [Category.{v} C]
+variable {J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [Category.{v} C]
   [HasZeroMorphisms C] [HasFiniteBiproducts C] {f : J → C} {g : K → C}
 
 /-- Convert a (dependently typed) matrix to a morphism of biproducts.
@@ -1031,8 +1034,7 @@ theorem biproduct.components_matrix (m : ⨁ f ⟶ ⨁ g) :
 
 /-- Morphisms between direct sums are matrices. -/
 @[simps]
-def biproduct.matrixEquiv : (⨁ f ⟶ ⨁ g) ≃ ∀ j k, f j ⟶ g k
-    where
+def biproduct.matrixEquiv : (⨁ f ⟶ ⨁ g) ≃ ∀ j k, f j ⟶ g k where
   toFun := biproduct.components
   invFun := biproduct.matrix
   left_inv := biproduct.components_matrix

Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean

@@ -163,13 +163,11 @@ variable {J : Type v}
 
 namespace WidePullbackShape
 
-instance fintypeObj [Fintype J] : Fintype (WidePullbackShape J) := by
-  rw [WidePullbackShape]
-  infer_instance
+instance fintypeObj [Fintype J] : Fintype (WidePullbackShape J) :=
+  instFintypeOption
 #align category_theory.limits.wide_pullback_shape.fintype_obj CategoryTheory.Limits.WidePullbackShape.fintypeObj
 
-instance fintypeHom (j j' : WidePullbackShape J) : Fintype (j ⟶ j')
-    where
+instance fintypeHom (j j' : WidePullbackShape J) : Fintype (j ⟶ j') where
   elems := by
     cases' j' with j'
     · cases' j with j
@@ -226,12 +224,11 @@ for every finite collection of morphisms
 -/
 class HasFiniteWidePullbacks : Prop where
   /-- `C` has all wide pullbacks any Fintype `J`-/
-  out (J : Type) [Fintype J] : HasLimitsOfShape (WidePullbackShape J) C
+  out (J : Type) [Finite J] : HasLimitsOfShape (WidePullbackShape J) C
 #align category_theory.limits.has_finite_wide_pullbacks CategoryTheory.Limits.HasFiniteWidePullbacks
 
 instance hasLimitsOfShape_widePullbackShape (J : Type) [Finite J] [HasFiniteWidePullbacks C] :
     HasLimitsOfShape (WidePullbackShape J) C := by
-  cases nonempty_fintype J
   haveI := @HasFiniteWidePullbacks.out C _ _ J
   infer_instance
 #align category_theory.limits.has_limits_of_shape_wide_pullback_shape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape
@@ -241,12 +238,11 @@ for every finite collection of morphisms
 -/
 class HasFiniteWidePushouts : Prop where
   /-- `C` has all wide pushouts any Fintype `J`-/
-  out (J : Type) [Fintype J] : HasColimitsOfShape (WidePushoutShape J) C
+  out (J : Type) [Finite J] : HasColimitsOfShape (WidePushoutShape J) C
 #align category_theory.limits.has_finite_wide_pushouts CategoryTheory.Limits.HasFiniteWidePushouts
 
 instance hasColimitsOfShape_widePushoutShape (J : Type) [Finite J] [HasFiniteWidePushouts C] :
     HasColimitsOfShape (WidePushoutShape J) C := by
-  cases nonempty_fintype J
   haveI := @HasFiniteWidePushouts.out C _ _ J
   infer_instance
 #align category_theory.limits.has_colimits_of_shape_wide_pushout_shape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape
@@ -255,15 +251,15 @@ instance hasColimitsOfShape_widePushoutShape (J : Type) [Finite J] [HasFiniteWid
 it also has finite wide pullbacks
 -/
 theorem hasFiniteWidePullbacks_of_hasFiniteLimits [HasFiniteLimits C] : HasFiniteWidePullbacks C :=
-  ⟨fun _ _ => HasFiniteLimits.out _⟩
+  ⟨fun J _ => by cases nonempty_fintype J; exact HasFiniteLimits.out _⟩
 #align category_theory.limits.has_finite_wide_pullbacks_of_has_finite_limits CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits
 
 /-- Finite wide pushouts are finite colimits, so if `C` has all finite colimits,
 it also has finite wide pushouts
 -/
 theorem hasFiniteWidePushouts_of_has_finite_limits [HasFiniteColimits C] :
     HasFiniteWidePushouts C :=
-  ⟨fun _ _ => HasFiniteColimits.out _⟩
+  ⟨fun J _ => by cases nonempty_fintype J; exact HasFiniteColimits.out _⟩
 #align category_theory.limits.has_finite_wide_pushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits
 
 instance fintypeWalkingPair : Fintype WalkingPair where

Mathlib/Data/Finite/Basic.lean

@@ -105,11 +105,6 @@ instance [Finite α] : Finite (Set α) := by
 
 end Finite
 
-/-- This instance also provides `[Finite s]` for `s : Set α`. -/
-instance Subtype.finite {α : Sort*} [Finite α] {p : α → Prop} : Finite { x // p x } :=
-  Finite.of_injective (↑) Subtype.coe_injective
-#align subtype.finite Subtype.finite
-
 instance Pi.finite {α : Sort*} {β : α → Sort*} [Finite α] [∀ a, Finite (β a)] :
     Finite (∀ a, β a) := by
   haveI := Fintype.ofFinite (PLift α)

Mathlib/Data/Fintype/Card.lean

@@ -450,12 +450,15 @@ noncomputable def Fintype.ofFinite (α : Type*) [Finite α] : Fintype α :=
 #align fintype.of_finite Fintype.ofFinite
 
 theorem Finite.of_injective {α β : Sort*} [Finite β] (f : α → β) (H : Injective f) : Finite α := by
-  cases nonempty_fintype (PLift β)
-  rw [← Equiv.injective_comp Equiv.plift f, ← Equiv.comp_injective _ Equiv.plift.symm] at H
-  haveI := Fintype.ofInjective _ H
-  exact Finite.of_equiv _ Equiv.plift
+  rcases Finite.exists_equiv_fin β with ⟨n, ⟨e⟩⟩
+  classical exact .of_equiv (Set.range (e ∘ f)) (Equiv.ofInjective _ (e.injective.comp H)).symm
 #align finite.of_injective Finite.of_injective
 
+/-- This instance also provides `[Finite s]` for `s : Set α`. -/
+instance Subtype.finite {α : Sort*} [Finite α] {p : α → Prop} : Finite { x // p x } :=
+  Finite.of_injective (↑) Subtype.coe_injective
+#align subtype.finite Subtype.finite
+
 theorem Finite.of_surjective {α β : Sort*} [Finite α] (f : α → β) (H : Surjective f) : Finite β :=
   Finite.of_injective _ <| injective_surjInv H
 #align finite.of_surjective Finite.of_surjective