feat(CategoryTheory/Limits): generalize universes for preserving fini…

…te products (#17408)

Mathlib/CategoryTheory/Limits/Preserves/Finite.lean

@@ -27,7 +27,7 @@ open CategoryTheory
 namespace CategoryTheory.Limits
 
 -- declare the `v`'s first; see `CategoryTheory.Category` for an explanation
-universe w w₂ v₁ v₂ v₃ u₁ u₂ u₃
+universe u w w₂ v₁ v₂ v₃ u₁ u₂ u₃
 
 variable {C : Type u₁} [Category.{v₁} C]
 variable {D : Type u₂} [Category.{v₂} D]
@@ -98,6 +98,12 @@ class PreservesFiniteProducts (F : C ⥤ D) where
 
 attribute [instance] PreservesFiniteProducts.preserves
 
+noncomputable instance (priority := 100) (F : C ⥤ D) (J : Type u) [Finite J]
+    [PreservesFiniteProducts F] : PreservesLimitsOfShape (Discrete J) F := by
+  apply Nonempty.some
+  obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J
+  exact ⟨preservesLimitsOfShapeOfEquiv (Discrete.equivalence e.symm) F⟩
+
 instance compPreservesFiniteProducts (F : C ⥤ D) (G : D ⥤ E)
     [PreservesFiniteProducts F] [PreservesFiniteProducts G] :
     PreservesFiniteProducts (F ⋙ G) where
@@ -243,14 +249,15 @@ class PreservesFiniteCoproducts (F : C ⥤ D) where
   /-- preservation of colimits indexed by `Discrete J` when `[Fintype J]` -/
   preserves : ∀ (J : Type) [Fintype J], PreservesColimitsOfShape (Discrete J) F
 
-noncomputable instance (F : C ⥤ D) (J : Type*) [Finite J] [PreservesFiniteCoproducts F] :
-    PreservesColimitsOfShape (Discrete J) F := by
+attribute [instance] PreservesFiniteCoproducts.preserves
+
+noncomputable instance (priority := 100) (F : C ⥤ D) (J : Type u) [Finite J]
+    [PreservesFiniteCoproducts F] : PreservesColimitsOfShape (Discrete J) F := by
   apply Nonempty.some
   obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J
-  have : PreservesColimitsOfShape (Discrete (Fin n)) F := PreservesFiniteCoproducts.preserves _
   exact ⟨preservesColimitsOfShapeOfEquiv (Discrete.equivalence e.symm) F⟩
 
-noncomputable instance compPreservesFiniteCoproducts (F : C ⥤ D) (G : D ⥤ E)
+instance compPreservesFiniteCoproducts (F : C ⥤ D) (G : D ⥤ E)
     [PreservesFiniteCoproducts F] [PreservesFiniteCoproducts G] :
     PreservesFiniteCoproducts (F ⋙ G) where
   preserves _ _ := inferInstance

Mathlib/Topology/Category/CompHausLike/SigmaComparison.lean

@@ -38,10 +38,6 @@ values on the components.
 def sigmaComparison : X.obj ⟨(of P ((a : α) × σ a))⟩ ⟶ ((a : α) → X.obj ⟨of P (σ a)⟩) :=
   fun x a ↦ X.map ⟨Sigma.mk a, continuous_sigmaMk⟩ x
 
-noncomputable instance : PreservesLimitsOfShape (Discrete α) X :=
-  letI : Fintype α := Fintype.ofFinite _
-  preservesFiniteProductsOfPreservesBinaryAndTerminal X α
-
 theorem sigmaComparison_eq_comp_isos : sigmaComparison X σ =
     (X.mapIso (opCoproductIsoProduct'
       (finiteCoproduct.isColimit.{u, u} (fun a ↦ of P (σ a)))