diff --git a/Mathlib/CategoryTheory/Adjunction/Limits.lean b/Mathlib/CategoryTheory/Adjunction/Limits.lean
index 7a7f509c021c3..c9f2595f1ad61 100644
--- a/Mathlib/CategoryTheory/Adjunction/Limits.lean
+++ b/Mathlib/CategoryTheory/Adjunction/Limits.lean
@@ -155,13 +155,13 @@ instance (priority := 100) isEquivalenceCreatesColimits (H : D ⥤ C) [IsEquival
 
 -- verify the preserve_colimits instance works as expected:
 example (E : C ⥤ D) [IsEquivalence E] (c : Cocone K) (h : IsColimit c) :
-    IsColimit (Functor.mapCocone E c) :=
+    IsColimit (E.mapCocone c) :=
   PreservesColimit.preserves h
 
 theorem hasColimit_comp_equivalence (E : C ⥤ D) [IsEquivalence E] [HasColimit K] :
     HasColimit (K ⋙ E) :=
   HasColimit.mk
-    { cocone := Functor.mapCocone E (colimit.cocone K)
+    { cocone := E.mapCocone (colimit.cocone K)
       isColimit := PreservesColimit.preserves (colimit.isColimit K) }
 #align category_theory.adjunction.has_colimit_comp_equivalence CategoryTheory.Adjunction.hasColimit_comp_equivalence
 
@@ -291,12 +291,12 @@ instance (priority := 100) isEquivalenceCreatesLimits (H : D ⥤ C) [IsEquivalen
 #align category_theory.adjunction.is_equivalence_creates_limits CategoryTheory.Adjunction.isEquivalenceCreatesLimits
 
 -- verify the preserve_limits instance works as expected:
-example (E : D ⥤ C) [IsEquivalence E] (c : Cone K) (h : IsLimit c) : IsLimit (mapCone E c) :=
+example (E : D ⥤ C) [IsEquivalence E] (c : Cone K) (h : IsLimit c) : IsLimit (E.mapCone c) :=
   PreservesLimit.preserves h
 
 theorem hasLimit_comp_equivalence (E : D ⥤ C) [IsEquivalence E] [HasLimit K] : HasLimit (K ⋙ E) :=
   HasLimit.mk
-    { cone := Functor.mapCone E (limit.cone K)
+    { cone := E.mapCone (limit.cone K)
       isLimit := PreservesLimit.preserves (limit.isLimit K) }
 #align category_theory.adjunction.has_limit_comp_equivalence CategoryTheory.Adjunction.hasLimit_comp_equivalence
 
diff --git a/Mathlib/CategoryTheory/Limits/Creates.lean b/Mathlib/CategoryTheory/Limits/Creates.lean
index 5ee1cb9679672..008966202efed 100644
--- a/Mathlib/CategoryTheory/Limits/Creates.lean
+++ b/Mathlib/CategoryTheory/Limits/Creates.lean
@@ -47,7 +47,7 @@ structure LiftableCone (K : J ⥤ C) (F : C ⥤ D) (c : Cone (K ⋙ F)) where
   /-- a cone in the source category of the functor -/
   liftedCone : Cone K
   /-- the isomorphism expressing that `liftedCone` lifts the given cone -/
-  validLift : Functor.mapCone F liftedCone ≅ c
+  validLift : F.mapCone liftedCone ≅ c
 #align category_theory.liftable_cone CategoryTheory.LiftableCone
 
 /-- Define the lift of a cocone: For a cocone `c` for `K ⋙ F`, give a cocone for
@@ -62,7 +62,7 @@ structure LiftableCocone (K : J ⥤ C) (F : C ⥤ D) (c : Cocone (K ⋙ F)) wher
   /-- a cocone in the source category of the functor -/
   liftedCocone : Cocone K
   /-- the isomorphism expressing that `liftedCocone` lifts the given cocone -/
-  validLift : Functor.mapCocone F liftedCocone ≅ c
+  validLift : F.mapCocone liftedCocone ≅ c
 #align category_theory.liftable_cocone CategoryTheory.LiftableCocone
 
 /-- Definition 3.3.1 of [Riehl].
@@ -144,7 +144,7 @@ def liftLimit {K : J ⥤ C} {F : C ⥤ D} [CreatesLimit K F] {c : Cone (K ⋙ F)
 
 /-- The lifted cone has an image isomorphic to the original cone. -/
 def liftedLimitMapsToOriginal {K : J ⥤ C} {F : C ⥤ D} [CreatesLimit K F] {c : Cone (K ⋙ F)}
-    (t : IsLimit c) : Functor.mapCone F (liftLimit t) ≅ c :=
+    (t : IsLimit c) : F.mapCone (liftLimit t) ≅ c :=
   (CreatesLimit.lifts c t).validLift
 #align category_theory.lifted_limit_maps_to_original CategoryTheory.liftedLimitMapsToOriginal
 
@@ -185,7 +185,7 @@ def liftColimit {K : J ⥤ C} {F : C ⥤ D} [CreatesColimit K F] {c : Cocone (K
 
 /-- The lifted cocone has an image isomorphic to the original cocone. -/
 def liftedColimitMapsToOriginal {K : J ⥤ C} {F : C ⥤ D} [CreatesColimit K F] {c : Cocone (K ⋙ F)}
-    (t : IsColimit c) : Functor.mapCocone F (liftColimit t) ≅ c :=
+    (t : IsColimit c) : F.mapCocone (liftColimit t) ≅ c :=
   (CreatesColimit.lifts c t).validLift
 #align category_theory.lifted_colimit_maps_to_original CategoryTheory.liftedColimitMapsToOriginal
 
@@ -267,10 +267,10 @@ def createsLimitOfReflectsIso {K : J ⥤ C} {F : C ⥤ D} [ReflectsIsomorphisms
   lifts c t := (h c t).toLiftableCone
   toReflectsLimit :=
     { reflects := fun {d} hd => by
-        let d' : Cone K := (h (Functor.mapCone F d) hd).toLiftableCone.liftedCone
-        let i : Functor.mapCone F d' ≅ Functor.mapCone F d :=
-          (h (Functor.mapCone F d) hd).toLiftableCone.validLift
-        let hd' : IsLimit d' := (h (Functor.mapCone F d) hd).makesLimit
+        let d' : Cone K := (h (F.mapCone d) hd).toLiftableCone.liftedCone
+        let i : F.mapCone d' ≅ F.mapCone d :=
+          (h (F.mapCone d) hd).toLiftableCone.validLift
+        let hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
         let f : d ⟶ d' := hd'.liftConeMorphism d
         have : (Cones.functoriality K F).map f = i.inv :=
           (hd.ofIsoLimit i.symm).uniq_cone_morphism
@@ -290,7 +290,7 @@ When `F` is fully faithful, to show that `F` creates the limit for `K` it suffic
 of a limit cone for `K ⋙ F`.
 -/
 def createsLimitOfFullyFaithfulOfLift' {K : J ⥤ C} {F : C ⥤ D} [Full F] [Faithful F]
-    {l : Cone (K ⋙ F)} (hl : IsLimit l) (c : Cone K) (i : Functor.mapCone F c ≅ l) :
+    {l : Cone (K ⋙ F)} (hl : IsLimit l) (c : Cone K) (i : F.mapCone c ≅ l) :
     CreatesLimit K F :=
   createsLimitOfReflectsIso fun _ t =>
     { liftedCone := c
@@ -306,7 +306,7 @@ def createsLimitOfFullyFaithfulOfLift' {K : J ⥤ C} {F : C ⥤ D} [Full F] [Fai
 it suffices to exhibit a lift of the chosen limit cone for `K ⋙ F`.
 -/
 def createsLimitOfFullyFaithfulOfLift {K : J ⥤ C} {F : C ⥤ D} [Full F] [Faithful F]
-    [HasLimit (K ⋙ F)] (c : Cone K) (i : Functor.mapCone F c ≅ limit.cone (K ⋙ F)) :
+    [HasLimit (K ⋙ F)] (c : Cone K) (i : F.mapCone c ≅ limit.cone (K ⋙ F)) :
     CreatesLimit K F :=
   createsLimitOfFullyFaithfulOfLift' (limit.isLimit _) c i
 #align category_theory.creates_limit_of_fully_faithful_of_lift CategoryTheory.createsLimitOfFullyFaithfulOfLift
@@ -375,10 +375,10 @@ def createsColimitOfReflectsIso {K : J ⥤ C} {F : C ⥤ D} [ReflectsIsomorphism
   toReflectsColimit :=
     {
       reflects := fun {d} hd => by
-        let d' : Cocone K := (h (Functor.mapCocone F d) hd).toLiftableCocone.liftedCocone
-        let i : Functor.mapCocone F d' ≅ Functor.mapCocone F d :=
-          (h (Functor.mapCocone F d) hd).toLiftableCocone.validLift
-        let hd' : IsColimit d' := (h (Functor.mapCocone F d) hd).makesColimit
+        let d' : Cocone K := (h (F.mapCocone d) hd).toLiftableCocone.liftedCocone
+        let i : F.mapCocone d' ≅ F.mapCocone d :=
+          (h (F.mapCocone d) hd).toLiftableCocone.validLift
+        let hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
         let f : d' ⟶ d := hd'.descCoconeMorphism d
         have : (Cocones.functoriality K F).map f = i.hom :=
           (hd.ofIsoColimit i.symm).uniq_cocone_morphism
@@ -398,7 +398,7 @@ When `F` is fully faithful, to show that `F` creates the colimit for `K` it suff
 lift of a colimit cocone for `K ⋙ F`.
 -/
 def createsColimitOfFullyFaithfulOfLift' {K : J ⥤ C} {F : C ⥤ D} [Full F] [Faithful F]
-    {l : Cocone (K ⋙ F)} (hl : IsColimit l) (c : Cocone K) (i : Functor.mapCocone F c ≅ l) :
+    {l : Cocone (K ⋙ F)} (hl : IsColimit l) (c : Cocone K) (i : F.mapCocone c ≅ l) :
     CreatesColimit K F :=
   createsColimitOfReflectsIso fun _ t =>
     { liftedCocone := c
@@ -415,7 +415,7 @@ When `F` is fully faithful, and `HasColimit (K ⋙ F)`, to show that `F` creates
 it suffices to exhibit a lift of the chosen colimit cocone for `K ⋙ F`.
 -/
 def createsColimitOfFullyFaithfulOfLift {K : J ⥤ C} {F : C ⥤ D} [Full F] [Faithful F]
-    [HasColimit (K ⋙ F)] (c : Cocone K) (i : Functor.mapCocone F c ≅ colimit.cocone (K ⋙ F)) :
+    [HasColimit (K ⋙ F)] (c : Cocone K) (i : F.mapCocone c ≅ colimit.cocone (K ⋙ F)) :
     CreatesColimit K F :=
   createsColimitOfFullyFaithfulOfLift' (colimit.isColimit _) c i
 #align category_theory.creates_colimit_of_fully_faithful_of_lift CategoryTheory.createsColimitOfFullyFaithfulOfLift
diff --git a/Mathlib/CategoryTheory/Limits/FunctorCategory.lean b/Mathlib/CategoryTheory/Limits/FunctorCategory.lean
index c4fe69e06c23b..8efede9ccddd6 100644
--- a/Mathlib/CategoryTheory/Limits/FunctorCategory.lean
+++ b/Mathlib/CategoryTheory/Limits/FunctorCategory.lean
@@ -53,7 +53,7 @@ it suffices to show that each evaluation cone is a limit. In other words, to pro
 limiting you can show it's pointwise limiting.
 -/
 def evaluationJointlyReflectsLimits {F : J ⥤ K ⥤ C} (c : Cone F)
-    (t : ∀ k : K, IsLimit (Functor.mapCone ((evaluation K C).obj k) c)) : IsLimit c
+    (t : ∀ k : K, IsLimit (((evaluation K C).obj k).mapCone c)) : IsLimit c
     where
   lift s :=
     { app := fun k => (t k).lift ⟨s.pt.obj k, whiskerRight s.π ((evaluation K C).obj k)⟩
@@ -94,7 +94,7 @@ def combineCones (F : J ⥤ K ⥤ C) (c : ∀ k : K, LimitCone (F.flip.obj k)) :
 
 /-- The stitched together cones each project down to the original given cones (up to iso). -/
 def evaluateCombinedCones (F : J ⥤ K ⥤ C) (c : ∀ k : K, LimitCone (F.flip.obj k)) (k : K) :
-    Functor.mapCone ((evaluation K C).obj k) (combineCones F c) ≅ (c k).cone :=
+    ((evaluation K C).obj k).mapCone (combineCones F c) ≅ (c k).cone :=
   Cones.ext (Iso.refl _) (by aesop_cat)
 #align category_theory.limits.evaluate_combined_cones CategoryTheory.Limits.evaluateCombinedCones
 
@@ -110,7 +110,7 @@ it suffices to show that each evaluation cocone is a colimit. In other words, to
 colimiting you can show it's pointwise colimiting.
 -/
 def evaluationJointlyReflectsColimits {F : J ⥤ K ⥤ C} (c : Cocone F)
-    (t : ∀ k : K, IsColimit (Functor.mapCocone ((evaluation K C).obj k) c)) : IsColimit c
+    (t : ∀ k : K, IsColimit (((evaluation K C).obj k).mapCocone  c)) : IsColimit c
     where
   desc s :=
     { app := fun k => (t k).desc ⟨s.pt.obj k, whiskerRight s.ι ((evaluation K C).obj k)⟩
@@ -155,7 +155,7 @@ def combineCocones (F : J ⥤ K ⥤ C) (c : ∀ k : K, ColimitCocone (F.flip.obj
 
 /-- The stitched together cocones each project down to the original given cocones (up to iso). -/
 def evaluateCombinedCocones (F : J ⥤ K ⥤ C) (c : ∀ k : K, ColimitCocone (F.flip.obj k)) (k : K) :
-    Functor.mapCocone ((evaluation K C).obj k) (combineCocones F c) ≅ (c k).cocone :=
+    ((evaluation K C).obj k).mapCocone  (combineCocones F c) ≅ (c k).cocone :=
   Cocones.ext (Iso.refl _) (by aesop_cat)
 #align category_theory.limits.evaluate_combined_cocones CategoryTheory.Limits.evaluateCombinedCocones
 
@@ -340,7 +340,7 @@ def preservesLimitOfEvaluation (F : D ⥤ K ⥤ C) (G : J ⥤ D)
     apply evaluationJointlyReflectsLimits
     intro X
     haveI := H X
-    change IsLimit (Functor.mapCone (F ⋙  (evaluation K C).obj X) c)
+    change IsLimit ((F ⋙  (evaluation K C).obj X).mapCone c)
     exact PreservesLimit.preserves hc⟩
 #align category_theory.limits.preserves_limit_of_evaluation CategoryTheory.Limits.preservesLimitOfEvaluation
 
@@ -377,7 +377,7 @@ def preservesColimitOfEvaluation (F : D ⥤ K ⥤ C) (G : J ⥤ D)
     apply evaluationJointlyReflectsColimits
     intro X
     haveI := H X
-    change IsColimit (Functor.mapCocone (F ⋙ (evaluation K C).obj X) c)
+    change IsColimit ((F ⋙ (evaluation K C).obj X).mapCocone c)
     exact PreservesColimit.preserves hc⟩
 #align category_theory.limits.preserves_colimit_of_evaluation CategoryTheory.Limits.preservesColimitOfEvaluation
 
diff --git a/Mathlib/CategoryTheory/Limits/HasLimits.lean b/Mathlib/CategoryTheory/Limits/HasLimits.lean
index 046ad86a358b2..59fa79e3dfa3a 100644
--- a/Mathlib/CategoryTheory/Limits/HasLimits.lean
+++ b/Mathlib/CategoryTheory/Limits/HasLimits.lean
@@ -458,7 +458,7 @@ variable (F) [HasLimit F] (G : C ⥤ D) [HasLimit (F ⋙ G)]
 /-- The canonical morphism from `G` applied to the limit of `F` to the limit of `F ⋙ G`.
 -/
 def limit.post : G.obj (limit F) ⟶ limit (F ⋙ G) :=
-  limit.lift (F ⋙ G) (mapCone G (limit.cone F))
+  limit.lift (F ⋙ G) (G.mapCone (limit.cone F))
 #align category_theory.limits.limit.post CategoryTheory.Limits.limit.post
 
 @[reassoc (attr := simp)]
@@ -469,7 +469,7 @@ theorem limit.post_π (j : J) : limit.post F G ≫ limit.π (F ⋙ G) j = G.map
 
 @[simp]
 theorem limit.lift_post (c : Cone F) :
-    G.map (limit.lift F c) ≫ limit.post F G = limit.lift (F ⋙ G) (mapCone G c) := by
+    G.map (limit.lift F c) ≫ limit.post F G = limit.lift (F ⋙ G) (G.mapCone c) := by
   ext
   rw [assoc, limit.post_π, ← G.map_comp, limit.lift_π, limit.lift_π]
   rfl
@@ -1038,7 +1038,7 @@ variable (F) [HasColimit F] (G : C ⥤ D) [HasColimit (F ⋙ G)]
 to `G` applied to the colimit of `F`.
 -/
 def colimit.post : colimit (F ⋙ G) ⟶ G.obj (colimit F) :=
-  colimit.desc (F ⋙ G) (mapCocone G (colimit.cocone F))
+  colimit.desc (F ⋙ G) (G.mapCocone (colimit.cocone F))
 #align category_theory.limits.colimit.post CategoryTheory.Limits.colimit.post
 
 @[reassoc (attr := simp)]
@@ -1050,7 +1050,7 @@ theorem colimit.ι_post (j : J) : colimit.ι (F ⋙ G) j ≫ colimit.post F G =
 
 @[simp]
 theorem colimit.post_desc (c : Cocone F) :
-    colimit.post F G ≫ G.map (colimit.desc F c) = colimit.desc (F ⋙ G) (mapCocone G c) := by
+    colimit.post F G ≫ G.map (colimit.desc F c) = colimit.desc (F ⋙ G) (G.mapCocone c) := by
   ext
   rw [← assoc, colimit.ι_post, ← G.map_comp, colimit.ι_desc, colimit.ι_desc]
   rfl
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Basic.lean b/Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
index c8c5a38cd8242..a136190629f9e 100644
--- a/Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
+++ b/Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
@@ -57,14 +57,14 @@ variable {J : Type w} [Category.{w'} J] {K : J ⥤ C}
 if `F` maps any limit cone over `K` to a limit cone.
 -/
 class PreservesLimit (K : J ⥤ C) (F : C ⥤ D) where
-  preserves : ∀ {c : Cone K}, IsLimit c → IsLimit (Functor.mapCone F c)
+  preserves : ∀ {c : Cone K}, IsLimit c → IsLimit (F.mapCone c)
 #align category_theory.limits.preserves_limit CategoryTheory.Limits.PreservesLimit
 
 /-- A functor `F` preserves colimits of `K` (written as `PreservesColimit K F`)
 if `F` maps any colimit cocone over `K` to a colimit cocone.
 -/
 class PreservesColimit (K : J ⥤ C) (F : C ⥤ D) where
-  preserves : ∀ {c : Cocone K}, IsColimit c → IsColimit (Functor.mapCocone F c)
+  preserves : ∀ {c : Cocone K}, IsColimit c → IsColimit (F.mapCocone c)
 #align category_theory.limits.preserves_colimit CategoryTheory.Limits.PreservesColimit
 
 /-- We say that `F` preserves limits of shape `J` if `F` preserves limits for every diagram
@@ -123,7 +123,7 @@ attribute [instance]
 guide typeclass resolution.
 -/
 def isLimitOfPreserves (F : C ⥤ D) {c : Cone K} (t : IsLimit c) [PreservesLimit K F] :
-    IsLimit (Functor.mapCone F c) :=
+    IsLimit (F.mapCone c) :=
   PreservesLimit.preserves t
 #align category_theory.limits.is_limit_of_preserves CategoryTheory.Limits.isLimitOfPreserves
 
@@ -132,7 +132,7 @@ A convenience function for `PreservesColimit`, which takes the functor as an exp
 guide typeclass resolution.
 -/
 def isColimitOfPreserves (F : C ⥤ D) {c : Cocone K} (t : IsColimit c) [PreservesColimit K F] :
-    IsColimit (Functor.mapCocone F c) :=
+    IsColimit (F.mapCocone c) :=
   PreservesColimit.preserves t
 #align category_theory.limits.is_colimit_of_preserves CategoryTheory.Limits.isColimitOfPreserves
 
@@ -229,7 +229,7 @@ end
 /-- If F preserves one limit cone for the diagram K,
   then it preserves any limit cone for K. -/
 def preservesLimitOfPreservesLimitCone {F : C ⥤ D} {t : Cone K} (h : IsLimit t)
-    (hF : IsLimit (Functor.mapCone F t)) : PreservesLimit K F :=
+    (hF : IsLimit (F.mapCone t)) : PreservesLimit K F :=
   ⟨fun h' => IsLimit.ofIsoLimit hF (Functor.mapIso _ (IsLimit.uniqueUpToIso h h'))⟩
 #align category_theory.limits.preserves_limit_of_preserves_limit_cone CategoryTheory.Limits.preservesLimitOfPreservesLimitCone
 
@@ -293,7 +293,7 @@ def preservesSmallestLimitsOfPreservesLimits (F : C ⥤ D) [PreservesLimitsOfSiz
 /-- If F preserves one colimit cocone for the diagram K,
   then it preserves any colimit cocone for K. -/
 def preservesColimitOfPreservesColimitCocone {F : C ⥤ D} {t : Cocone K} (h : IsColimit t)
-    (hF : IsColimit (Functor.mapCocone F t)) : PreservesColimit K F :=
+    (hF : IsColimit (F.mapCocone t)) : PreservesColimit K F :=
   ⟨fun h' => IsColimit.ofIsoColimit hF (Functor.mapIso _ (IsColimit.uniqueUpToIso h h'))⟩
 #align category_theory.limits.preserves_colimit_of_preserves_colimit_cocone CategoryTheory.Limits.preservesColimitOfPreservesColimitCocone
 
@@ -362,7 +362,7 @@ the cone was already a limit cone in `C`.
 Note that we do not assume a priori that `D` actually has any limits.
 -/
 class ReflectsLimit (K : J ⥤ C) (F : C ⥤ D) where
-  reflects : ∀ {c : Cone K}, IsLimit (Functor.mapCone F c) → IsLimit c
+  reflects : ∀ {c : Cone K}, IsLimit (F.mapCone c) → IsLimit c
 #align category_theory.limits.reflects_limit CategoryTheory.Limits.ReflectsLimit
 
 /-- A functor `F : C ⥤ D` reflects colimits for `K : J ⥤ C` if
@@ -371,7 +371,7 @@ the cocone was already a colimit cocone in `C`.
 Note that we do not assume a priori that `D` actually has any colimits.
 -/
 class ReflectsColimit (K : J ⥤ C) (F : C ⥤ D) where
-  reflects : ∀ {c : Cocone K}, IsColimit (Functor.mapCocone F c) → IsColimit c
+  reflects : ∀ {c : Cocone K}, IsColimit (F.mapCocone c) → IsColimit c
 #align category_theory.limits.reflects_colimit CategoryTheory.Limits.ReflectsColimit
 
 /-- A functor `F : C ⥤ D` reflects limits of shape `J` if
@@ -437,7 +437,7 @@ abbrev ReflectsColimits (F : C ⥤ D) :=
 /-- A convenience function for `ReflectsLimit`, which takes the functor as an explicit argument to
 guide typeclass resolution.
 -/
-def isLimitOfReflects (F : C ⥤ D) {c : Cone K} (t : IsLimit (Functor.mapCone F c))
+def isLimitOfReflects (F : C ⥤ D) {c : Cone K} (t : IsLimit (F.mapCone c))
     [ReflectsLimit K F] : IsLimit c := ReflectsLimit.reflects t
 #align category_theory.limits.is_limit_of_reflects CategoryTheory.Limits.isLimitOfReflects
 
@@ -445,7 +445,7 @@ def isLimitOfReflects (F : C ⥤ D) {c : Cone K} (t : IsLimit (Functor.mapCone F
 A convenience function for `ReflectsColimit`, which takes the functor as an explicit argument to
 guide typeclass resolution.
 -/
-def isColimitOfReflects (F : C ⥤ D) {c : Cocone K} (t : IsColimit (Functor.mapCocone F c))
+def isColimitOfReflects (F : C ⥤ D) {c : Cocone K} (t : IsColimit (F.mapCocone c))
     [ReflectsColimit K F] : IsColimit c :=
   ReflectsColimit.reflects t
 #align category_theory.limits.is_colimit_of_reflects CategoryTheory.Limits.isColimitOfReflects
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Limits.lean b/Mathlib/CategoryTheory/Limits/Preserves/Limits.lean
index 9681688061cf9..0e423d2582a7d 100644
--- a/Mathlib/CategoryTheory/Limits/Preserves/Limits.lean
+++ b/Mathlib/CategoryTheory/Limits/Preserves/Limits.lean
@@ -47,8 +47,8 @@ variable [PreservesLimit F G]
 
 @[simp]
 theorem preserves_lift_mapCone (c₁ c₂ : Cone F) (t : IsLimit c₁) :
-    (PreservesLimit.preserves t).lift (Functor.mapCone G c₂) = G.map (t.lift c₂) :=
-  ((PreservesLimit.preserves t).uniq (Functor.mapCone G c₂) _ (by simp [← G.map_comp])).symm
+    (PreservesLimit.preserves t).lift (G.mapCone c₂) = G.map (t.lift c₂) :=
+  ((PreservesLimit.preserves t).uniq (G.mapCone c₂) _ (by simp [← G.map_comp])).symm
 #align category_theory.preserves_lift_map_cone CategoryTheory.preserves_lift_mapCone
 
 variable [HasLimit F] [HasLimit (F ⋙ G)]
@@ -75,7 +75,7 @@ theorem preservesLimitsIso_inv_π (j) :
 @[reassoc (attr := simp)]
 theorem lift_comp_preservesLimitsIso_hom (t : Cone F) :
     G.map (limit.lift _ t) ≫ (preservesLimitIso G F).hom = 
-    limit.lift (F ⋙ G) (Functor.mapCone G _) := by
+    limit.lift (F ⋙ G) (G.mapCone _) := by
   ext
   simp [← G.map_comp]
 #align category_theory.lift_comp_preserves_limits_iso_hom CategoryTheory.lift_comp_preservesLimitsIso_hom
@@ -103,8 +103,8 @@ variable [PreservesColimit F G]
 
 @[simp]
 theorem preserves_desc_mapCocone (c₁ c₂ : Cocone F) (t : IsColimit c₁) :
-    (PreservesColimit.preserves t).desc (Functor.mapCocone G _) = G.map (t.desc c₂) := 
-  ((PreservesColimit.preserves t).uniq (Functor.mapCocone G _) _ (by simp [← G.map_comp])).symm
+    (PreservesColimit.preserves t).desc (G.mapCocone _) = G.map (t.desc c₂) := 
+  ((PreservesColimit.preserves t).uniq (G.mapCocone _) _ (by simp [← G.map_comp])).symm
 #align category_theory.preserves_desc_map_cocone CategoryTheory.preserves_desc_mapCocone
 
 variable [HasColimit F] [HasColimit (F ⋙ G)]
@@ -132,7 +132,7 @@ theorem ι_preservesColimitsIso_hom (j : J) :
 @[reassoc (attr := simp)]
 theorem preservesColimitsIso_inv_comp_desc (t : Cocone F) :
     (preservesColimitIso G F).inv ≫ G.map (colimit.desc _ t) = 
-    colimit.desc _ (Functor.mapCocone G t) := by
+    colimit.desc _ (G.mapCocone t) := by
   ext
   simp [← G.map_comp]
 #align category_theory.preserves_colimits_iso_inv_comp_desc CategoryTheory.preservesColimitsIso_inv_comp_desc
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/BinaryProducts.lean b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/BinaryProducts.lean
index 959907cd89ea6..8bac41104f38f 100644
--- a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/BinaryProducts.lean
+++ b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/BinaryProducts.lean
@@ -45,7 +45,7 @@ The map of a binary fan is a limit iff the fork consisting of the mapped morphis
 essentially lets us commute `BinaryFan.mk` with `Functor.mapCone`.
 -/
 def isLimitMapConeBinaryFanEquiv :
-    IsLimit (Functor.mapCone G (BinaryFan.mk f g)) ≃ IsLimit (BinaryFan.mk (G.map f) (G.map g)) :=
+    IsLimit (G.mapCone (BinaryFan.mk f g)) ≃ IsLimit (BinaryFan.mk (G.map f) (G.map g)) :=
   (IsLimit.postcomposeHomEquiv (diagramIsoPair _) _).symm.trans
     (IsLimit.equivIsoLimit
       (Cones.ext (Iso.refl _)
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean
index f903097fa584a..ced7e8f7ce79d 100644
--- a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean
+++ b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean
@@ -43,7 +43,7 @@ section Terminal
 /-- The map of an empty cone is a limit iff the mapped object is terminal.
 -/
 def isLimitMapConeEmptyConeEquiv :
-    IsLimit (Functor.mapCone G (asEmptyCone X)) ≃ IsTerminal (G.obj X) :=
+    IsLimit (G.mapCone (asEmptyCone X)) ≃ IsTerminal (G.obj X) :=
   isLimitEmptyConeEquiv D _ _ (eqToIso rfl)
 #align category_theory.limits.is_limit_map_cone_empty_cone_equiv CategoryTheory.Limits.isLimitMapConeEmptyConeEquiv
 
@@ -136,7 +136,7 @@ section Initial
 /-- The map of an empty cocone is a colimit iff the mapped object is initial.
 -/
 def isColimitMapCoconeEmptyCoconeEquiv :
-    IsColimit (Functor.mapCocone G (asEmptyCocone.{v₁} X)) ≃ IsInitial (G.obj X) :=
+    IsColimit (G.mapCocone (asEmptyCocone.{v₁} X)) ≃ IsInitial (G.obj X) :=
   isColimitEmptyCoconeEquiv D _ _ (eqToIso rfl)
 #align category_theory.limits.is_colimit_map_cocone_empty_cocone_equiv CategoryTheory.Limits.isColimitMapCoconeEmptyCoconeEquiv
 
diff --git a/Mathlib/CategoryTheory/Limits/Yoneda.lean b/Mathlib/CategoryTheory/Limits/Yoneda.lean
index a6f536ebf7344..475ee4137d858 100644
--- a/Mathlib/CategoryTheory/Limits/Yoneda.lean
+++ b/Mathlib/CategoryTheory/Limits/Yoneda.lean
@@ -121,7 +121,7 @@ instance coyonedaPreservesLimits (X : Cᵒᵖ) : PreservesLimits (coyoneda.obj X
 
 /-- The yoneda embeddings jointly reflect limits. -/
 def yonedaJointlyReflectsLimits (J : Type w) [SmallCategory J] (K : J ⥤ Cᵒᵖ) (c : Cone K)
-    (t : ∀ X : C, IsLimit (Functor.mapCone (yoneda.obj X) c)) : IsLimit c :=
+    (t : ∀ X : C, IsLimit ((yoneda.obj X).mapCone c)) : IsLimit c :=
   let s' : ∀ s : Cone K, Cone (K ⋙ yoneda.obj s.pt.unop) := fun s =>
     ⟨PUnit, fun j _ => (s.π.app j).unop, fun j₁ j₂ α =>
       funext fun _ => Quiver.Hom.op_inj (s.w α).symm⟩
@@ -139,7 +139,7 @@ def yonedaJointlyReflectsLimits (J : Type w) [SmallCategory J] (K : J ⥤ Cᵒ
 
 /-- The coyoneda embeddings jointly reflect limits. -/
 def coyonedaJointlyReflectsLimits (J : Type w) [SmallCategory J] (K : J ⥤ C) (c : Cone K)
-    (t : ∀ X : Cᵒᵖ, IsLimit (Functor.mapCone (coyoneda.obj X) c)) : IsLimit c :=
+    (t : ∀ X : Cᵒᵖ, IsLimit ((coyoneda.obj X).mapCone c)) : IsLimit c :=
   let s' : ∀ s : Cone K, Cone (K ⋙ coyoneda.obj (op s.pt)) := fun s =>
     ⟨PUnit, fun j _ => s.π.app j, fun j₁ j₂ α => funext fun _ => (s.w α).symm⟩
   { lift := fun s => (t (op s.pt)).lift (s' s) PUnit.unit