diff --git a/Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean b/Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
index 305a3bbd5a648..0b2e0d72e2f6e 100644
--- a/Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
+++ b/Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
@@ -146,18 +146,23 @@ def combinedIsColimit (F : J ⥤ K ⥤ C) (c : ∀ k : K, ColimitCocone (F.flip.
 
 noncomputable section
 
+instance functorCategoryHasLimit (F : J ⥤ K ⥤ C) [∀ k, HasLimit (F.flip.obj k)] : HasLimit F :=
+  HasLimit.mk
+    { cone := combineCones F fun _ => getLimitCone _
+      isLimit := combinedIsLimit _ _ }
+
 instance functorCategoryHasLimitsOfShape [HasLimitsOfShape J C] : HasLimitsOfShape J (K ⥤ C) where
-  has_limit F :=
-    HasLimit.mk
-      { cone := combineCones F fun _ => getLimitCone _
-        isLimit := combinedIsLimit _ _ }
+  has_limit _ := inferInstance
+
+instance functorCategoryHasColimit (F : J ⥤ K ⥤ C) [∀ k, HasColimit (F.flip.obj k)] :
+    HasColimit F :=
+  HasColimit.mk
+    { cocone := combineCocones F fun _ => getColimitCocone _
+      isColimit := combinedIsColimit _ _ }
 
 instance functorCategoryHasColimitsOfShape [HasColimitsOfShape J C] :
     HasColimitsOfShape J (K ⥤ C) where
-  has_colimit _ :=
-    HasColimit.mk
-      { cocone := combineCocones _ fun _ => getColimitCocone _
-        isColimit := combinedIsColimit _ _ }
+  has_colimit _ := inferInstance
 
 -- Porting note: previously Lean could see through the binders and infer_instance sufficed
 instance functorCategoryHasLimitsOfSize [HasLimitsOfSize.{v₁, u₁} C] :
@@ -169,14 +174,20 @@ instance functorCategoryHasColimitsOfSize [HasColimitsOfSize.{v₁, u₁} C] :
     HasColimitsOfSize.{v₁, u₁} (K ⥤ C) where
   has_colimits_of_shape := fun _ _ => inferInstance
 
+instance hasLimitCompEvalution (F : J ⥤ K ⥤ C) (k : K) [HasLimit (F.flip.obj k)] :
+    HasLimit (F ⋙ (evaluation _ _).obj k) :=
+  hasLimitOfIso (F := F.flip.obj k) (Iso.refl _)
+
+instance evaluationPreservesLimit (F : J ⥤ K ⥤ C) [∀ k, HasLimit (F.flip.obj k)] (k : K) :
+    PreservesLimit F ((evaluation K C).obj k) :=
+    -- Porting note: added a let because X was not inferred
+  let X : (k : K) → LimitCone (F.flip.obj k) := fun k => getLimitCone (F.flip.obj k)
+  preservesLimitOfPreservesLimitCone (combinedIsLimit _ X) <|
+    IsLimit.ofIsoLimit (limit.isLimit _) (evaluateCombinedCones F X k).symm
+
 instance evaluationPreservesLimitsOfShape [HasLimitsOfShape J C] (k : K) :
     PreservesLimitsOfShape J ((evaluation K C).obj k) where
-  preservesLimit {F} := by
-    -- Porting note: added a let because X was not inferred
-    let X : (k : K) → LimitCone (Prefunctor.obj (Functor.flip F).toPrefunctor k) :=
-      fun k => getLimitCone (Prefunctor.obj (Functor.flip F).toPrefunctor k)
-    exact preservesLimitOfPreservesLimitCone (combinedIsLimit _ _) <|
-      IsLimit.ofIsoLimit (limit.isLimit _) (evaluateCombinedCones F X k).symm
+  preservesLimit := inferInstance
 
 /-- If `F : J ⥤ K ⥤ C` is a functor into a functor category which has a limit,
 then the evaluation of that limit at `k` is the limit of the evaluations of `F.obj j` at `k`.
@@ -225,14 +236,20 @@ theorem limit_obj_ext {H : J ⥤ K ⥤ C} [HasLimitsOfShape J C] {k : K} {W : C}
   ext j
   simpa using w j
 
+instance hasColimitCompEvaluation (F : J ⥤ K ⥤ C) (k : K) [HasColimit (F.flip.obj k)] :
+    HasColimit (F ⋙ (evaluation _ _).obj k) :=
+  hasColimitOfIso (F := F.flip.obj k) (Iso.refl _)
+
+instance evaluationPreservesColimit (F : J ⥤ K ⥤ C) [∀ k, HasColimit (F.flip.obj k)] (k : K) :
+    PreservesColimit F ((evaluation K C).obj k) :=
+  -- Porting note: added a let because X was not inferred
+  let X : (k : K) → ColimitCocone (F.flip.obj k) := fun k => getColimitCocone (F.flip.obj k)
+  preservesColimitOfPreservesColimitCocone (combinedIsColimit _ X) <|
+    IsColimit.ofIsoColimit (colimit.isColimit _) (evaluateCombinedCocones F X k).symm
+
 instance evaluationPreservesColimitsOfShape [HasColimitsOfShape J C] (k : K) :
     PreservesColimitsOfShape J ((evaluation K C).obj k) where
-  preservesColimit {F} := by
-    -- Porting note: added a let because X was not inferred
-    let X : (k : K) → ColimitCocone (Prefunctor.obj (Functor.flip F).toPrefunctor k) :=
-      fun k => getColimitCocone (Prefunctor.obj (Functor.flip F).toPrefunctor k)
-    refine preservesColimitOfPreservesColimitCocone (combinedIsColimit _ _) <|
-      IsColimit.ofIsoColimit (colimit.isColimit _) (evaluateCombinedCocones F X k).symm
+  preservesColimit := inferInstance
 
 /-- If `F : J ⥤ K ⥤ C` is a functor into a functor category which has a colimit,
 then the evaluation of that colimit at `k` is the colimit of the evaluations of `F.obj j` at `k`.
diff --git a/Mathlib/CategoryTheory/Limits/FunctorToTypes.lean b/Mathlib/CategoryTheory/Limits/FunctorToTypes.lean
index 62eb96c6be392..ba9abc78c25d6 100644
--- a/Mathlib/CategoryTheory/Limits/FunctorToTypes.lean
+++ b/Mathlib/CategoryTheory/Limits/FunctorToTypes.lean
@@ -20,15 +20,20 @@ open CategoryTheory.Limits
 universe w v₁ v₂ u₁ u₂
 
 variable {J : Type u₁} [Category.{v₁} J] {K : Type u₂} [Category.{v₂} K]
-variable (F : J ⥤ K ⥤ TypeMax.{u₁, w})
+variable (F : J ⥤ K ⥤ Type w)
 
-theorem jointly_surjective (k : K) {t : Cocone F} (h : IsColimit t) (x : t.pt.obj k) :
-    ∃ j y, x = (t.ι.app j).app k y := by
+theorem jointly_surjective (k : K) {t : Cocone F} (h : IsColimit t) (x : t.pt.obj k)
+    [∀ k, HasColimit (F.flip.obj k)] : ∃ j y, x = (t.ι.app j).app k y := by
   let hev := isColimitOfPreserves ((evaluation _ _).obj k) h
   obtain ⟨j, y, rfl⟩ := Types.jointly_surjective _ hev x
   exact ⟨j, y, by simp⟩
 
-theorem jointly_surjective' (k : K) (x : (colimit F).obj k) : ∃ j y, x = (colimit.ι F j).app k y :=
+theorem jointly_surjective' [∀ k, HasColimit (F.flip.obj k)] (k : K) (x : (colimit F).obj k) :
+    ∃ j y, x = (colimit.ι F j).app k y :=
   jointly_surjective _ _ (colimit.isColimit _) x
 
+theorem colimit.map_ι_apply [HasColimit F] (j : J) {k k' : K} {f : k ⟶ k'} {x} :
+    (colimit F).map f ((colimit.ι F j).app _ x) = (colimit.ι F j).app _ ((F.obj j).map f x) :=
+  congrFun ((colimit.ι F j).naturality _).symm _
+
 end CategoryTheory.FunctorToTypes