chore(CategoryTheory/Presentable/Basic): remove bad instance (leanprover-community#41660)

The instance `HasCardinalFilteredColimits.hasColimitsOfShape` is bad because it has no way to infer the value of `κ`.

Almost 2 years ago there was a change to type classes, which caused Lean to not give a warning about this, in leanprover/lean4#5376 and I think that is an issue.

This PR is a copy of leanprover-community#27941. In the meantime, this instance has accidentally been added again in leanprover-community#30533.

Author: JovanGerb

Mathlib/CategoryTheory/Presentable/Adjunction.lean

@@ -86,8 +86,9 @@ lemma isCardinalLocallyPresentable [IsCardinalLocallyPresentable C κ]
 lemma isCardinalAccessibleCategory [IsCardinalAccessibleCategory C κ]
     [G.IsCardinalAccessible κ] [G.Full] [G.Faithful] :
     IsCardinalAccessibleCategory D κ where
-  toHasCardinalFilteredColimits := ⟨fun _ _ _ ↦
+  toHasCardinalFilteredColimits := ⟨fun J _ _ ↦
     let : Reflective G := ⟨_, adj⟩
+    have := HasCardinalFilteredColimits.hasColimitsOfShape C κ J
     hasColimitsOfShape_of_reflective G⟩
   toHasCardinalFilteredGenerator := adj.hasCardinalFilteredGenerator κ
 

Mathlib/CategoryTheory/Presentable/Basic.lean

@@ -344,17 +344,15 @@ end
 
 section
 
-variable (C) (κ : Cardinal.{w}) [Fact κ.IsRegular]
-
 /-- A category has `κ`-filtered colimits if it has colimits of shape `J`
 for any `κ`-filtered category `J`. -/
-class HasCardinalFilteredColimits : Prop where
-  hasColimitsOfShape (J : Type w) [SmallCategory J] [IsCardinalFiltered J κ] :
+class HasCardinalFilteredColimits (C : Type u₁) [Category.{v₁} C]
+    (κ : Cardinal.{w}) [Fact κ.IsRegular] : Prop where
+  hasColimitsOfShape (C) (J : Type w) [SmallCategory J] [IsCardinalFiltered J κ] :
     HasColimitsOfShape J C := by intros; infer_instance
 
-attribute [instance] HasCardinalFilteredColimits.hasColimitsOfShape
-
-instance [HasColimitsOfSize.{w, w} C] : HasCardinalFilteredColimits.{w} C κ where
+instance (κ : Cardinal.{w}) [Fact κ.IsRegular] [HasColimitsOfSize.{w, w} C] :
+    HasCardinalFilteredColimits.{w} C κ where
 
 end
 

Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean

@@ -99,6 +99,7 @@ lemma MorphismProperty.isCardinalAccessible_ι_isLocal
     W.isLocal.ι.IsCardinalAccessible κ where
   preservesColimitOfShape J _ _ := by
     have := W.isClosedUnderColimitsOfShape_isLocal J κ hW
+    have := HasCardinalFilteredColimits.hasColimitsOfShape C κ J
     infer_instance
 
 namespace OrthogonalReflection