chore(CategoryTheory/EssentiallySmall): adding an instance (#30534)

joelriou · joelriou · commit 807c88463ae3 · 2025-10-28T20:32:22.000Z
Before this PR, `example (C : Type w) [SmallCategory C] : EssentiallySmall.{w} C := inferInstance` would not work. We fix this by making `essentiallySmall_of_small_of_locallySmall` an instance.

Consequently, we need to make certain universes explicit in a few proofs. Some instances in `Sites.Equivalence` are transformed into lemmas because it seems they shadowed more basic instances.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -3127,6 +3127,7 @@ import Mathlib.Condensed.Light.CartesianClosed
 import Mathlib.Condensed.Light.Epi
 import Mathlib.Condensed.Light.Explicit
 import Mathlib.Condensed.Light.Functors
+import Mathlib.Condensed.Light.Instances
 import Mathlib.Condensed.Light.Limits
 import Mathlib.Condensed.Light.Module
 import Mathlib.Condensed.Light.Small
diff --git a/Mathlib/Algebra/Category/Grp/Subobject.lean b/Mathlib/Algebra/Category/Grp/Subobject.lean
@@ -18,6 +18,6 @@ universe u
 namespace AddCommGrpCat
 
 instance wellPowered_addCommGrp : WellPowered.{u} AddCommGrpCat.{u} :=
-  wellPowered_of_equiv (forget₂ (ModuleCat.{u} ℤ) AddCommGrpCat.{u}).asEquivalence
+  wellPowered_of_equiv.{u} (forget₂ (ModuleCat.{u} ℤ) AddCommGrpCat.{u}).asEquivalence
 
 end AddCommGrpCat
diff --git a/Mathlib/AlgebraicGeometry/Modules/Presheaf.lean b/Mathlib/AlgebraicGeometry/Modules/Presheaf.lean
@@ -28,7 +28,7 @@ variable (X : Scheme.{u})
 
 /-- The underlying sheaf of rings of a scheme. -/
 abbrev ringCatSheaf : TopCat.Sheaf RingCat.{u} X :=
-  (sheafCompose _ (forget₂ CommRingCat RingCat)).obj X.sheaf
+  (sheafCompose _ (forget₂ CommRingCat RingCat.{u})).obj X.sheaf
 
 /-- The category of presheaves of modules over a scheme. -/
 nonrec abbrev PresheafOfModules := PresheafOfModules.{u} X.ringCatSheaf.val
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
@@ -310,9 +310,9 @@ lemma AB5OfSize_of_univLE [HasFilteredColimitsOfSize.{w₂, w₂'} C] [UnivLE.{w
   constructor
   intro J _ _
   haveI := IsFiltered.of_equivalence ((ShrinkHoms.equivalence.{w₂} J).trans <|
-    Shrink.equivalence.{w₂'} (ShrinkHoms.{w'} J))
+    Shrink.equivalence.{w₂', w₂} (ShrinkHoms.{w'} J))
   exact HasExactColimitsOfShape.of_domain_equivalence _ ((ShrinkHoms.equivalence.{w₂} J).trans <|
-    Shrink.equivalence.{w₂'} (ShrinkHoms.{w'} J)).symm
+    Shrink.equivalence.{w₂', w₂} (ShrinkHoms.{w'} J)).symm
 
 lemma AB5OfSize_shrink [HasFilteredColimitsOfSize.{max w w₂, max w' w₂'} C]
     [AB5OfSize.{max w w₂, max w' w₂'} C] :
@@ -344,9 +344,9 @@ lemma AB5StarOfSize_of_univLE [HasCofilteredLimitsOfSize.{w₂, w₂'} C] [UnivL
   constructor
   intro J _ _
   haveI := IsCofiltered.of_equivalence ((ShrinkHoms.equivalence.{w₂} J).trans <|
-    Shrink.equivalence.{w₂'} (ShrinkHoms.{w'} J))
+    Shrink.equivalence.{w₂', w₂} (ShrinkHoms.{w'} J))
   exact HasExactLimitsOfShape.of_domain_equivalence _ ((ShrinkHoms.equivalence.{w₂} J).trans <|
-    Shrink.equivalence.{w₂'} (ShrinkHoms.{w'} J)).symm
+    Shrink.equivalence.{w₂', w₂} (ShrinkHoms.{w'} J)).symm
 
 lemma AB5StarOfSize_shrink [HasCofilteredLimitsOfSize.{max w w₂, max w' w₂'} C]
     [AB5StarOfSize.{max w w₂, max w' w₂'} C] :
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Sheaf.lean
@@ -69,7 +69,9 @@ instance {C : Type v} [SmallCategory.{v} C] (J : GrothendieckTopology C)
     (A : Type u₁) [Category.{v} A] [Abelian A] [IsGrothendieckAbelian.{v} A]
     [HasSheafify J A] : IsGrothendieckAbelian.{v} (Sheaf J A) where
 
-instance {C : Type (v + 1)} [LargeCategory C] [EssentiallySmall.{v} C]
+attribute [local instance] hasSheafifyEssentiallySmallSite in
+lemma isGrothendieckAbelian_of_essentiallySmall
+    {C : Type u₂} [Category.{v} C] [EssentiallySmall.{v} C]
     (J : GrothendieckTopology C)
     (A : Type u₁) [Category.{v} A] [Abelian A] [IsGrothendieckAbelian.{v} A]
     [HasSheafify ((equivSmallModel C).inverse.inducedTopology J) A] :
diff --git a/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean b/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
@@ -105,7 +105,7 @@ lemma isRightAdjoint_of_preservesLimits_of_isCoseparating [HasLimits D] [WellPow
     (hP : P.IsCoseparating) (G : D ⥤ C) [PreservesLimits G] :
     G.IsRightAdjoint := by
   have : ∀ A, HasInitial (StructuredArrow A G) := fun A ↦
-    hasInitial_of_isCoseparating (StructuredArrow.isCoseparating_inverseImage_proj A G hP)
+    hasInitial_of_isCoseparating.{v} (StructuredArrow.isCoseparating_inverseImage_proj A G hP)
   exact isRightAdjointOfStructuredArrowInitials _
 
 /-- The special adjoint functor theorem: if `F : C ⥤ D` preserves colimits and `C` is cocomplete,
@@ -116,7 +116,7 @@ lemma isLeftAdjoint_of_preservesColimits_of_isSeparating [HasColimits C] [WellPo
     (h𝒢 : P.IsSeparating) (F : C ⥤ D) [PreservesColimits F] :
     F.IsLeftAdjoint :=
   have : ∀ A, HasTerminal (CostructuredArrow F A) := fun A =>
-    hasTerminal_of_isSeparating (CostructuredArrow.isSeparating_inverseImage_proj F A h𝒢)
+    hasTerminal_of_isSeparating.{v} (CostructuredArrow.isSeparating_inverseImage_proj F A h𝒢)
   isLeftAdjoint_of_costructuredArrowTerminals _
 
 end SpecialAdjointFunctorTheorem
diff --git a/Mathlib/CategoryTheory/EssentiallySmall.lean b/Mathlib/CategoryTheory/EssentiallySmall.lean
@@ -227,10 +227,12 @@ theorem essentiallySmall_iff (C : Type u) [Category.{v} C] :
       (skeletonEquivalence (ShrinkHoms C)).symm.trans
         ((inducedFunctor (e'.trans e).symm).asEquivalence.symm)
 
-theorem essentiallySmall_of_small_of_locallySmall [Small.{w} C] [LocallySmall.{w} C] :
+instance essentiallySmall_of_small_of_locallySmall [Small.{w} C] [LocallySmall.{w} C] :
     EssentiallySmall.{w} C :=
   (essentiallySmall_iff C).2 ⟨small_of_surjective Quotient.exists_rep, by infer_instance⟩
 
+example (C : Type w) [SmallCategory C] : EssentiallySmall.{w} C := inferInstance
+
 instance small_skeleton_of_essentiallySmall [h : EssentiallySmall.{w} C] : Small.{w} (Skeleton C) :=
   essentiallySmall_iff C |>.1 h |>.1
 
diff --git a/Mathlib/CategoryTheory/Generator/Abelian.lean b/Mathlib/CategoryTheory/Generator/Abelian.lean
@@ -33,7 +33,7 @@ variable {C : Type u} [Category.{v} C] [Abelian C]
 theorem has_injective_coseparator [HasLimits C] [EnoughInjectives C] (G : C) (hG : IsSeparator G) :
     ∃ G : C, Injective G ∧ IsCoseparator G := by
   haveI : WellPowered.{v} C := wellPowered_of_isDetector G hG.isDetector
-  haveI : HasProductsOfShape (Subobject (op G)) C := hasProductsOfShape_of_small _ _
+  haveI : HasProductsOfShape (Subobject (op G)) C := hasProductsOfShape_of_small.{v} _ _
   let T : C := Injective.under (piObj fun P : Subobject (op G) => unop P)
   refine ⟨T, inferInstance, (Preadditive.isCoseparator_iff _).2 fun X Y f hf => ?_⟩
   refine (Preadditive.isSeparator_iff _).1 hG _ fun h => ?_
diff --git a/Mathlib/CategoryTheory/Limits/Filtered.lean b/Mathlib/CategoryTheory/Limits/Filtered.lean
@@ -108,9 +108,9 @@ lemma hasCofilteredLimitsOfSize_of_univLE [UnivLE.{w, w₂}] [UnivLE.{w', w₂'}
     HasCofilteredLimitsOfSize.{w', w} C where
   HasLimitsOfShape J :=
     haveI := IsCofiltered.of_equivalence ((ShrinkHoms.equivalence.{w₂'} J).trans <|
-      Shrink.equivalence.{w₂} (ShrinkHoms.{w} J))
+      Shrink.equivalence.{w₂, w₂'} (ShrinkHoms.{w} J))
     hasLimitsOfShape_of_equivalence ((ShrinkHoms.equivalence.{w₂'} J).trans <|
-      Shrink.equivalence.{w₂} (ShrinkHoms.{w} J)).symm
+      Shrink.equivalence.{w₂, w₂'} (ShrinkHoms.{w} J)).symm
 
 lemma hasCofilteredLimitsOfSize_shrink [HasCofilteredLimitsOfSize.{max w' w₂', max w w₂} C] :
     HasCofilteredLimitsOfSize.{w', w} C :=
@@ -121,9 +121,9 @@ lemma hasFilteredColimitsOfSize_of_univLE [UnivLE.{w, w₂}] [UnivLE.{w', w₂'}
     HasFilteredColimitsOfSize.{w', w} C where
   HasColimitsOfShape J :=
     haveI := IsFiltered.of_equivalence ((ShrinkHoms.equivalence.{w₂'} J).trans <|
-      Shrink.equivalence.{w₂} (ShrinkHoms.{w} J))
+      Shrink.equivalence.{w₂, w₂'} (ShrinkHoms.{w} J))
     hasColimitsOfShape_of_equivalence ((ShrinkHoms.equivalence.{w₂'} J).trans <|
-      Shrink.equivalence.{w₂} (ShrinkHoms.{w} J)).symm
+      Shrink.equivalence.{w₂, w₂'} (ShrinkHoms.{w} J)).symm
 
 lemma hasFilteredColimitsOfSize_shrink [HasFilteredColimitsOfSize.{max w' w₂', max w w₂} C] :
     HasFilteredColimitsOfSize.{w', w} C :=
diff --git a/Mathlib/CategoryTheory/Limits/HasLimits.lean b/Mathlib/CategoryTheory/Limits/HasLimits.lean
@@ -571,7 +571,7 @@ variable (C)
 theorem hasLimitsOfSizeOfUnivLE [UnivLE.{v₂, v₁}] [UnivLE.{u₂, u₁}]
     [HasLimitsOfSize.{v₁, u₁} C] : HasLimitsOfSize.{v₂, u₂} C where
   has_limits_of_shape J {_} := hasLimitsOfShape_of_equivalence
-    ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm
+    ((ShrinkHoms.equivalence.{v₁} J).trans <| Shrink.equivalence _).symm
 
 /-- `hasLimitsOfSizeShrink.{v u} C` tries to obtain `HasLimitsOfSize.{v u} C`
 from some other `HasLimitsOfSize C`.
@@ -1086,7 +1086,7 @@ variable (C)
 theorem hasColimitsOfSizeOfUnivLE [UnivLE.{v₂, v₁}] [UnivLE.{u₂, u₁}]
     [HasColimitsOfSize.{v₁, u₁} C] : HasColimitsOfSize.{v₂, u₂} C where
   has_colimits_of_shape J {_} := hasColimitsOfShape_of_equivalence
-    ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm
+    ((ShrinkHoms.equivalence.{v₁} J).trans <| Shrink.equivalence _).symm
 
 /-- `hasColimitsOfSizeShrink.{v u} C` tries to obtain `HasColimitsOfSize.{v u} C`
 from some other `HasColimitsOfSize C`.
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Basic.lean b/Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
@@ -238,7 +238,7 @@ lemma preservesLimitsOfShape_of_equiv {J' : Type w₂} [Category.{w₂'} J'] (e
 lemma preservesLimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
     [PreservesLimitsOfSize.{w', w₂'} F] : PreservesLimitsOfSize.{w, w₂} F where
   preservesLimitsOfShape {J} := preservesLimitsOfShape_of_equiv
-    ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm F
+    ((ShrinkHoms.equivalence.{w'} J).trans <| Shrink.equivalence _).symm F
 
 /-- `PreservesLimitsOfSize_shrink.{w w'} F` tries to obtain `PreservesLimitsOfSize.{w w'} F`
 from some other `PreservesLimitsOfSize F`.
@@ -297,7 +297,7 @@ lemma preservesColimitsOfShape_of_equiv {J' : Type w₂} [Category.{w₂'} J'] (
 lemma preservesColimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
     [PreservesColimitsOfSize.{w', w₂'} F] : PreservesColimitsOfSize.{w, w₂} F where
   preservesColimitsOfShape {J} := preservesColimitsOfShape_of_equiv
-    ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm F
+    ((ShrinkHoms.equivalence.{w'} J).trans <| Shrink.equivalence _).symm F
 
 /--
 `PreservesColimitsOfSize_shrink.{w w'} F` tries to obtain `PreservesColimitsOfSize.{w w'} F`
@@ -543,7 +543,7 @@ lemma reflectsLimitsOfShape_of_equiv {J' : Type w₂} [Category.{w₂'} J'] (e :
 lemma reflectsLimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
     [ReflectsLimitsOfSize.{w', w₂'} F] : ReflectsLimitsOfSize.{w, w₂} F where
   reflectsLimitsOfShape {J} := reflectsLimitsOfShape_of_equiv
-    ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm F
+    ((ShrinkHoms.equivalence.{w'} J).trans <| Shrink.equivalence _).symm F
 
 /-- `reflectsLimitsOfSize_shrink.{w w'} F` tries to obtain `reflectsLimitsOfSize.{w w'} F`
 from some other `reflectsLimitsOfSize F`.
@@ -646,7 +646,7 @@ lemma reflectsColimitsOfShape_of_equiv {J' : Type w₂} [Category.{w₂'} J'] (e
 lemma reflectsColimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
     [ReflectsColimitsOfSize.{w', w₂'} F] : ReflectsColimitsOfSize.{w, w₂} F where
   reflectsColimitsOfShape {J} := reflectsColimitsOfShape_of_equiv
-    ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm F
+    ((ShrinkHoms.equivalence.{w'} J).trans <| Shrink.equivalence _).symm F
 
 /-- `reflectsColimitsOfSize_shrink.{w w'} F` tries to obtain `reflectsColimitsOfSize.{w w'} F`
 from some other `reflectsColimitsOfSize F`.
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Filtered.lean b/Mathlib/CategoryTheory/Limits/Preserves/Filtered.lean
@@ -63,7 +63,7 @@ lemma preservesFilteredColimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}]
     [UnivLE.{w₂, w₂'}] [PreservesFilteredColimitsOfSize.{w', w₂'} F] :
       PreservesFilteredColimitsOfSize.{w, w₂} F where
   preserves_filtered_colimits J _ _ := by
-    let e := ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm
+    let e := ((ShrinkHoms.equivalence.{w'} J).trans <| Shrink.equivalence _).symm
     haveI := IsFiltered.of_equivalence e.symm
     exact preservesColimitsOfShape_of_equiv e F
 
@@ -119,7 +119,7 @@ lemma reflectsFilteredColimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}]
     [UnivLE.{w₂, w₂'}] [ReflectsFilteredColimitsOfSize.{w', w₂'} F] :
       ReflectsFilteredColimitsOfSize.{w, w₂} F where
   reflects_filtered_colimits J _ _ := by
-    let e := ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm
+    let e := ((ShrinkHoms.equivalence.{w'} J).trans <| Shrink.equivalence _).symm
     haveI := IsFiltered.of_equivalence e.symm
     exact reflectsColimitsOfShape_of_equiv e F
 
@@ -179,7 +179,7 @@ lemma preservesCofilteredLimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}]
     [UnivLE.{w₂, w₂'}] [PreservesCofilteredLimitsOfSize.{w', w₂'} F] :
       PreservesCofilteredLimitsOfSize.{w, w₂} F where
   preserves_cofiltered_limits J _ _ := by
-    let e := ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm
+    let e := ((ShrinkHoms.equivalence.{w'} J).trans <| Shrink.equivalence _).symm
     haveI := IsCofiltered.of_equivalence e.symm
     exact preservesLimitsOfShape_of_equiv e F
 
@@ -235,7 +235,7 @@ lemma reflectsCofilteredLimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}]
     [UnivLE.{w₂, w₂'}] [ReflectsCofilteredLimitsOfSize.{w', w₂'} F] :
       ReflectsCofilteredLimitsOfSize.{w, w₂} F where
   reflects_cofiltered_limits J _ _ := by
-    let e := ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm
+    let e := ((ShrinkHoms.equivalence.{w'} J).trans <| Shrink.equivalence _).symm
     haveI := IsCofiltered.of_equivalence e.symm
     exact reflectsLimitsOfShape_of_equiv e F
 
diff --git a/Mathlib/CategoryTheory/Sites/Equivalence.lean b/Mathlib/CategoryTheory/Sites/Equivalence.lean
@@ -188,13 +188,14 @@ noncomputable
 def smallSheafificationAdjunction : smallSheafify J A ⊣ sheafToPresheaf J A :=
   (equivSmallModel C).transportSheafificationAdjunction J _ A
 
-noncomputable instance hasSheafifyEssentiallySmallSite : HasSheafify J A :=
+lemma hasSheafifyEssentiallySmallSite : HasSheafify J A :=
   (equivSmallModel C).hasSheafify J ((equivSmallModel C).inverse.inducedTopology J) A
 
 instance hasSheafComposeEssentiallySmallSite : HasSheafCompose J F :=
   (equivSmallModel C).hasSheafCompose J ((equivSmallModel C).inverse.inducedTopology J) F
 
-instance hasLimitsEssentiallySmallSite
+omit [HasSheafify ((equivSmallModel C).inverse.inducedTopology J) A] in
+lemma hasLimitsEssentiallySmallSite
     [HasLimits <| Sheaf ((equivSmallModel C).inverse.inducedTopology J) A] :
     HasLimitsOfSize.{max v₃ w, max v₃ w} <| Sheaf J A :=
   Adjunction.has_limits_of_equivalence ((equivSmallModel C).sheafCongr J
@@ -283,7 +284,8 @@ lemma WEqualsLocallyBijective.transport (hG : CoverPreserving K J G) :
 variable [EssentiallySmall.{w} C]
   [∀ (X : Cᵒᵖ), HasLimitsOfShape (StructuredArrow X (equivSmallModel C).inverse.op) A]
 
-instance [((equivSmallModel C).inverse.inducedTopology J).WEqualsLocallyBijective A] :
+lemma WEqualsLocallyBijective.ofEssentiallySmall
+    [((equivSmallModel C).inverse.inducedTopology J).WEqualsLocallyBijective A] :
     J.WEqualsLocallyBijective A :=
   WEqualsLocallyBijective.transport J ((equivSmallModel C).inverse.inducedTopology J)
     (equivSmallModel C).inverse (IsDenseSubsite.coverPreserving _ _ _)
diff --git a/Mathlib/CategoryTheory/Sites/LeftExact.lean b/Mathlib/CategoryTheory/Sites/LeftExact.lean
@@ -292,6 +292,10 @@ instance [PreservesLimits (forget D)] [HasFiniteLimits D]
     HasSheafify J D :=
   HasSheafify.mk' J D (plusPlusAdjunction J D)
 
+attribute [local instance] Types.instFunLike Types.instConcreteCategory in
+instance : HasSheafify J (Type max u v) := by
+  infer_instance
+
 end
 
 variable {D : Type w} [Category.{w'} D]
diff --git a/Mathlib/CategoryTheory/Sites/PreservesSheafification.lean b/Mathlib/CategoryTheory/Sites/PreservesSheafification.lean
@@ -287,15 +287,15 @@ instance : PreservesSheafification J F := by
 end
 
 attribute [local instance] Types.instFunLike Types.instConcreteCategory in
-example {D : Type*} [Category.{max v u} D] {FD : D → D → Type*} {CD : D → Type (max v u)}
+instance {D : Type*} [Category.{max v u} D] {FD : D → D → Type*} {CD : D → Type (max v u)}
     [∀ X Y, FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory.{max v u} D FD]
     [PreservesLimits (forget D)]
     [∀ X : C, HasColimitsOfShape (J.Cover X)ᵒᵖ D]
     [∀ X : C, PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
     [∀ (J : MulticospanShape.{max v u, max v u}),
       Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) D]
     [(forget D).ReflectsIsomorphisms] : PreservesSheafification J (forget D) :=
-  instPreservesSheafification _ _
+  inferInstance
 
 end GrothendieckTopology
 
diff --git a/Mathlib/CategoryTheory/Sites/Whiskering.lean b/Mathlib/CategoryTheory/Sites/Whiskering.lean
@@ -117,7 +117,7 @@ end GrothendieckTopology.Cover
 Composing a sheaf with a functor preserving the limit of `(S.index P).multicospan` yields a functor
 between sheaf categories.
 -/
-instance hasSheafCompose_of_preservesMulticospan (F : A ⥤ B)
+instance (priority := high) hasSheafCompose_of_preservesMulticospan (F : A ⥤ B)
     [∀ (X : C) (S : J.Cover X) (P : Cᵒᵖ ⥤ A), PreservesLimit (S.index P).multicospan F] :
     J.HasSheafCompose F where
   isSheaf P hP := by
diff --git a/Mathlib/Condensed/Discrete/Basic.lean b/Mathlib/Condensed/Discrete/Basic.lean
@@ -7,6 +7,7 @@ import Mathlib.CategoryTheory.Sites.ConstantSheaf
 import Mathlib.CategoryTheory.Sites.Equivalence
 import Mathlib.Condensed.Basic
 import Mathlib.Condensed.Light.Basic
+import Mathlib.Condensed.Light.Instances
 /-!
 
 # Discrete-underlying adjunction
@@ -84,7 +85,6 @@ noncomputable def discreteUnderlyingAdj : discrete C ⊣ underlying C :=
 
 end LightCondensed
 
-attribute [local instance] Types.instFunLike Types.instConcreteCategory in
 /-- A version of `LightCondensed.discrete` in the `LightCondSet` namespace -/
 noncomputable abbrev LightCondSet.discrete := LightCondensed.discrete (Type u)
 
diff --git a/Mathlib/Condensed/Light/AB.lean b/Mathlib/Condensed/Light/AB.lean
@@ -29,6 +29,6 @@ noncomputable instance : CountableAB4Star (LightCondMod.{u} R) :=
   CountableAB4Star.of_hasExactLimitsOfShape_nat _
 
 instance : IsGrothendieckAbelian.{u} (LightCondMod.{u} R) :=
-  inferInstanceAs (IsGrothendieckAbelian.{u} (Sheaf _ _))
+  Sheaf.isGrothendieckAbelian_of_essentiallySmall _ _
 
 end LightCondensed
diff --git a/Mathlib/Condensed/Light/CartesianClosed.lean b/Mathlib/Condensed/Light/CartesianClosed.lean
@@ -7,6 +7,7 @@ import Mathlib.CategoryTheory.Closed.Types
 import Mathlib.CategoryTheory.Sites.CartesianClosed
 import Mathlib.CategoryTheory.Sites.Equivalence
 import Mathlib.Condensed.Light.Basic
+import Mathlib.Condensed.Light.Instances
 /-!
 
 # Light condensed sets form a Cartesian closed category
@@ -23,5 +24,4 @@ variable {C : Type u} [SmallCategory C]
 instance : CartesianMonoidalCategory (LightCondSet.{u}) :=
   inferInstanceAs (CartesianMonoidalCategory (Sheaf _ _))
 
-attribute [local instance] Types.instFunLike Types.instConcreteCategory in
 instance : CartesianClosed (LightCondSet.{u}) := inferInstanceAs (CartesianClosed (Sheaf _ _))
diff --git a/Mathlib/Condensed/Light/Instances.lean b/Mathlib/Condensed/Light/Instances.lean
@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.Topology.Category.LightProfinite.EffectiveEpi
+import Mathlib.CategoryTheory.Sites.Equivalence
+
+/-!
+# `HasSheafify` instances
+
+In this file, we obtain a `HasSheafify (coherentTopology LightProfinite.{u}) (Type u)`
+instance (and similarly for other concrete categories). These instances
+are not obtained automatically because `LightProfinite.{u}` is a large category,
+but as it is essentially small, the instances can be obtained using the results
+in the file `CategoryTheory.Sites.Equivalence`.
+
+-/
+
+universe u u' v
+
+open CategoryTheory Limits
+
+namespace LightProfinite
+
+variable (A : Type u') [Category.{u} A] [HasLimits A] [HasColimits A]
+  {FA : A → A → Type v} {CA : A → Type u}
+  [∀ X Y, FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory A FA]
+  [PreservesFilteredColimits (forget A)]
+  [PreservesLimits (forget A)] [(forget A).ReflectsIsomorphisms]
+
+instance hasSheafify :
+    HasSheafify (coherentTopology LightProfinite.{u}) A :=
+  hasSheafifyEssentiallySmallSite _ _
+
+instance hasSheafify_type :
+    HasSheafify (coherentTopology LightProfinite.{u}) (Type u) :=
+  hasSheafifyEssentiallySmallSite _ _
+
+instance : (coherentTopology LightProfinite.{u}).WEqualsLocallyBijective A :=
+  GrothendieckTopology.WEqualsLocallyBijective.ofEssentiallySmall _
+
+end LightProfinite
diff --git a/Mathlib/Condensed/Light/Module.lean b/Mathlib/Condensed/Light/Module.lean
@@ -11,6 +11,7 @@ import Mathlib.CategoryTheory.Sites.Abelian
 import Mathlib.CategoryTheory.Sites.Adjunction
 import Mathlib.CategoryTheory.Sites.Equivalence
 import Mathlib.Condensed.Light.Basic
+import Mathlib.Condensed.Light.Instances
 /-!
 
 # Light condensed `R`-modules
diff --git a/MathlibTest/CategoryTheory/Sites/ConcreteSheafification.lean b/MathlibTest/CategoryTheory/Sites/ConcreteSheafification.lean
@@ -29,8 +29,9 @@ example (R : Type (u + 1)) [Ring R] : HasSheafify J (ModuleCat.{u+1} R) := infer
 
 variable [EssentiallySmall.{u} C]
 
-example : HasSheafify J (Type u) := inferInstance
+example : HasSheafify J (Type u) := hasSheafifyEssentiallySmallSite _ _
 
-example (R : Type u) [Ring R] : HasSheafify J (ModuleCat.{u} R) := inferInstance
+example (R : Type u) [Ring R] : HasSheafify J (ModuleCat.{u} R) :=
+  hasSheafifyEssentiallySmallSite _ _
 
 end Large
