diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean
index ea25e5d1bf2f7..f58ed17c074ed 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean
@@ -68,17 +68,17 @@ noncomputable def colimitPresheafOfModules : PresheafOfModules R where
   map_id X := colimit.hom_ext (fun j => by
     dsimp
     rw [ι_colimMap_assoc, whiskerLeft_app, restriction_app]
-    erw [ι_preservesColimitsIso_inv (G := ModuleCat.restrictScalars (R.map (𝟙 X))),
+    erw [ι_preservesColimitIso_inv (G := ModuleCat.restrictScalars (R.map (𝟙 X))),
       ModuleCat.restrictScalarsId'App_inv_naturality]
     rw [map_id]
     dsimp)
   map_comp {X Y Z} f g := colimit.hom_ext (fun j => by
     dsimp
     rw [ι_colimMap_assoc, whiskerLeft_app, restriction_app, assoc, ι_colimMap_assoc]
-    erw [ι_preservesColimitsIso_inv (G := ModuleCat.restrictScalars (R.map (f ≫ g))),
-      ι_preservesColimitsIso_inv_assoc (G := ModuleCat.restrictScalars (R.map f))]
+    erw [ι_preservesColimitIso_inv (G := ModuleCat.restrictScalars (R.map (f ≫ g))),
+      ι_preservesColimitIso_inv_assoc (G := ModuleCat.restrictScalars (R.map f))]
     rw [← Functor.map_comp_assoc, ι_colimMap_assoc]
-    erw [ι_preservesColimitsIso_inv (G := ModuleCat.restrictScalars (R.map g))]
+    erw [ι_preservesColimitIso_inv (G := ModuleCat.restrictScalars (R.map g))]
     rw [map_comp, ModuleCat.restrictScalarsComp'_inv_app, assoc, assoc,
       whiskerLeft_app, whiskerLeft_app, restriction_app, restriction_app]
     simp only [Functor.map_comp, assoc]
@@ -94,7 +94,7 @@ noncomputable def colimitCocone : Cocone F where
         { app := fun X ↦ colimit.ι (F ⋙ evaluation R X) j
           naturality := fun {X Y} f ↦ by
             dsimp
-            erw [colimit.ι_desc_assoc, assoc, ← ι_preservesColimitsIso_inv]
+            erw [colimit.ι_desc_assoc, assoc, ← ι_preservesColimitIso_inv]
             rfl }
       naturality := fun {X Y} f ↦ by
         ext1 X
diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean
index 52757e35c210f..127f29b50a89e 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean
@@ -73,7 +73,7 @@ noncomputable def limitPresheafOfModules : PresheafOfModules R where
     dsimp
     simp only [limMap_π, Functor.comp_obj, evaluation_obj, whiskerLeft_app,
       restriction_app, assoc]
-    erw [preservesLimitsIso_hom_π]
+    erw [preservesLimitIso_hom_π]
     rw [← ModuleCat.restrictScalarsId'App_inv_naturality, map_id,
       ModuleCat.restrictScalarsId'_inv_app]
     dsimp
@@ -85,14 +85,14 @@ noncomputable def limitPresheafOfModules : PresheafOfModules R where
     intro j
     simp only [Functor.comp_obj, evaluation_obj, limMap_π, whiskerLeft_app, restriction_app,
       map_comp, ModuleCat.restrictScalarsComp'_inv_app, Functor.map_comp, assoc]
-    erw [preservesLimitsIso_hom_π]
+    erw [preservesLimitIso_hom_π]
     rw [← ModuleCat.restrictScalarsComp'App_inv_naturality]
     dsimp
     rw [← Functor.map_comp_assoc, ← Functor.map_comp_assoc, assoc,
-      preservesLimitsIso_inv_π]
+      preservesLimitIso_inv_π]
     erw [limMap_π]
     dsimp
-    simp only [Functor.map_comp, assoc, preservesLimitsIso_inv_π_assoc]
+    simp only [Functor.map_comp, assoc, preservesLimitIso_inv_π_assoc]
     erw [limMap_π_assoc]
     dsimp
 
@@ -106,7 +106,7 @@ noncomputable def limitCone : Cone F where
         { app := fun X ↦ limit.π (F ⋙ evaluation R X) j
           naturality := fun {X Y} f ↦ by
             dsimp
-            simp only [assoc, preservesLimitsIso_inv_π]
+            simp only [assoc, preservesLimitIso_inv_π]
             apply limMap_π }
       naturality := fun {j j'} f ↦ by
         ext1 X
diff --git a/Mathlib/CategoryTheory/GlueData.lean b/Mathlib/CategoryTheory/GlueData.lean
index b43f3893e3bca..433fa5d3d835c 100644
--- a/Mathlib/CategoryTheory/GlueData.lean
+++ b/Mathlib/CategoryTheory/GlueData.lean
@@ -318,7 +318,7 @@ def gluedIso : F.obj D.glued ≅ (D.mapGlueData F).glued :=
 @[reassoc (attr := simp)]
 theorem ι_gluedIso_hom (i : D.J) : F.map (D.ι i) ≫ (D.gluedIso F).hom = (D.mapGlueData F).ι i := by
   haveI : HasColimit (MultispanIndex.multispan (diagram (mapGlueData D F))) := inferInstance
-  erw [ι_preservesColimitsIso_hom_assoc]
+  erw [ι_preservesColimitIso_hom_assoc]
   rw [HasColimit.isoOfNatIso_ι_hom]
   erw [Category.id_comp]
   rfl
diff --git a/Mathlib/CategoryTheory/Limits/Elements.lean b/Mathlib/CategoryTheory/Limits/Elements.lean
index 84963f2bacdff..bea7b175e4f22 100644
--- a/Mathlib/CategoryTheory/Limits/Elements.lean
+++ b/Mathlib/CategoryTheory/Limits/Elements.lean
@@ -53,7 +53,7 @@ lemma map_lift_mapCone (c : Cone F) :
     A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd = liftedConeElement F := by
   apply (preservesLimitIso A (F ⋙ π A)).toEquiv.injective
   ext i
-  have h₁ := congrFun (preservesLimitsIso_hom_π A (F ⋙ π A) i)
+  have h₁ := congrFun (preservesLimitIso_hom_π A (F ⋙ π A) i)
     (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)
   have h₂ := (c.π.app i).property
   simp_all [← FunctorToTypes.map_comp_apply, liftedConeElement]
@@ -62,7 +62,7 @@ lemma map_lift_mapCone (c : Cone F) :
 lemma map_π_liftedConeElement (i : I) :
     A.map (limit.π (F ⋙ π A) i) (liftedConeElement F) = (F.obj i).snd := by
   have := congrFun
-    (preservesLimitsIso_inv_π A (F ⋙ π A) i) (liftedConeElement' F)
+    (preservesLimitIso_inv_π A (F ⋙ π A) i) (liftedConeElement' F)
   simp_all [liftedConeElement]
 
 /-- (implementation) The constructured limit cone. -/
diff --git a/Mathlib/CategoryTheory/Limits/IndYoneda.lean b/Mathlib/CategoryTheory/Limits/IndYoneda.lean
index 99842d2a0d02f..07f8ecd466bc2 100644
--- a/Mathlib/CategoryTheory/Limits/IndYoneda.lean
+++ b/Mathlib/CategoryTheory/Limits/IndYoneda.lean
@@ -94,7 +94,7 @@ lemma coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π (i : I) :
     (coyonedaOpColimitIsoLimitCoyoneda F).hom ≫ limit.π (F.op.comp coyoneda) ⟨i⟩
       = coyoneda.map (colimit.ι F i).op := by
   simp only [coyonedaOpColimitIsoLimitCoyoneda, Functor.mapIso_symm,
-    Iso.trans_hom, Iso.symm_hom, Functor.mapIso_inv, Category.assoc, preservesLimitsIso_hom_π,
+    Iso.trans_hom, Iso.symm_hom, Functor.mapIso_inv, Category.assoc, preservesLimitIso_hom_π,
     ← Functor.map_comp, limitOpIsoOpColimit_inv_comp_π]
 
 @[reassoc (attr := simp)]
@@ -142,7 +142,7 @@ lemma coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π (i : I) :
     (coyonedaOpColimitIsoLimitCoyoneda' F).hom ≫ limit.π (F.rightOp ⋙ coyoneda) i
       = coyoneda.map (colimit.ι F ⟨i⟩).op := by
   simp only [coyonedaOpColimitIsoLimitCoyoneda', Functor.mapIso_symm, Iso.trans_hom, Iso.symm_hom,
-    Functor.mapIso_inv, Category.assoc, preservesLimitsIso_hom_π, ← Functor.map_comp,
+    Functor.mapIso_inv, Category.assoc, preservesLimitIso_hom_π, ← Functor.map_comp,
     limitRightOpIsoOpColimit_inv_comp_π]
 
 @[reassoc (attr := simp)]
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Limits.lean b/Mathlib/CategoryTheory/Limits/Preserves/Limits.lean
index 10c785ddbe059..ac77b2c0bcd51 100644
--- a/Mathlib/CategoryTheory/Limits/Preserves/Limits.lean
+++ b/Mathlib/CategoryTheory/Limits/Preserves/Limits.lean
@@ -50,22 +50,29 @@ def preservesLimitIso : G.obj (limit F) ≅ limit (F ⋙ G) :=
   (PreservesLimit.preserves (limit.isLimit _)).conePointUniqueUpToIso (limit.isLimit _)
 
 @[reassoc (attr := simp)]
-theorem preservesLimitsIso_hom_π (j) :
+theorem preservesLimitIso_hom_π (j) :
     (preservesLimitIso G F).hom ≫ limit.π _ j = G.map (limit.π F j) :=
   IsLimit.conePointUniqueUpToIso_hom_comp _ _ j
 
+@[deprecated (since := "2024-10-27")] alias preservesLimitsIso_hom_π := preservesLimitIso_hom_π
+
 @[reassoc (attr := simp)]
-theorem preservesLimitsIso_inv_π (j) :
+theorem preservesLimitIso_inv_π (j) :
     (preservesLimitIso G F).inv ≫ G.map (limit.π F j) = limit.π _ j :=
   IsLimit.conePointUniqueUpToIso_inv_comp _ _ j
 
+@[deprecated (since := "2024-10-27")] alias preservesLimitsIso_inv_π := preservesLimitIso_inv_π
+
 @[reassoc (attr := simp)]
-theorem lift_comp_preservesLimitsIso_hom (t : Cone F) :
+theorem lift_comp_preservesLimitIso_hom (t : Cone F) :
     G.map (limit.lift _ t) ≫ (preservesLimitIso G F).hom =
     limit.lift (F ⋙ G) (G.mapCone _) := by
   ext
   simp [← G.map_comp]
 
+@[deprecated (since := "2024-10-27")]
+alias lift_comp_preservesLimitsIso_hom := lift_comp_preservesLimitIso_hom
+
 instance : IsIso (limit.post F G) :=
   show IsIso (preservesLimitIso G F).hom from inferInstance
 
@@ -80,8 +87,8 @@ def preservesLimitNatIso : lim ⋙ G ≅ (whiskeringRight J C D).obj G ⋙ lim :
       intro _ _ f
       apply limit.hom_ext; intro j
       dsimp
-      simp only [preservesLimitsIso_hom_π, whiskerRight_app, limMap_π, Category.assoc,
-        preservesLimitsIso_hom_π_assoc, ← G.map_comp])
+      simp only [preservesLimitIso_hom_π, whiskerRight_app, limMap_π, Category.assoc,
+        preservesLimitIso_hom_π_assoc, ← G.map_comp])
 
 end
 
@@ -117,22 +124,31 @@ def preservesColimitIso : G.obj (colimit F) ≅ colimit (F ⋙ G) :=
   (PreservesColimit.preserves (colimit.isColimit _)).coconePointUniqueUpToIso (colimit.isColimit _)
 
 @[reassoc (attr := simp)]
-theorem ι_preservesColimitsIso_inv (j : J) :
+theorem ι_preservesColimitIso_inv (j : J) :
     colimit.ι _ j ≫ (preservesColimitIso G F).inv = G.map (colimit.ι F j) :=
   IsColimit.comp_coconePointUniqueUpToIso_inv _ (colimit.isColimit (F ⋙ G)) j
 
+@[deprecated (since := "2024-10-27")]
+alias ι_preservesColimitsIso_inv := ι_preservesColimitIso_inv
+
 @[reassoc (attr := simp)]
-theorem ι_preservesColimitsIso_hom (j : J) :
+theorem ι_preservesColimitIso_hom (j : J) :
     G.map (colimit.ι F j) ≫ (preservesColimitIso G F).hom = colimit.ι (F ⋙ G) j :=
   (PreservesColimit.preserves (colimit.isColimit _)).comp_coconePointUniqueUpToIso_hom _ j
 
+@[deprecated (since := "2024-10-27")]
+alias ι_preservesColimitsIso_hom := ι_preservesColimitIso_hom
+
 @[reassoc (attr := simp)]
-theorem preservesColimitsIso_inv_comp_desc (t : Cocone F) :
+theorem preservesColimitIso_inv_comp_desc (t : Cocone F) :
     (preservesColimitIso G F).inv ≫ G.map (colimit.desc _ t) =
     colimit.desc _ (G.mapCocone t) := by
   ext
   simp [← G.map_comp]
 
+@[deprecated (since := "2024-10-27")]
+alias preservesColimitsIso_inv_comp_desc := preservesColimitIso_inv_comp_desc
+
 instance : IsIso (colimit.post F G) :=
   show IsIso (preservesColimitIso G F).inv from inferInstance
 
@@ -149,8 +165,8 @@ def preservesColimitNatIso : colim ⋙ G ≅ (whiskeringRight J C D).obj G ⋙ c
       apply colimit.hom_ext; intro j
       dsimp
       rw [ι_colimMap_assoc]
-      simp only [ι_preservesColimitsIso_inv, whiskerRight_app, Category.assoc,
-        ι_preservesColimitsIso_inv_assoc, ← G.map_comp]
+      simp only [ι_preservesColimitIso_inv, whiskerRight_app, Category.assoc,
+        ι_preservesColimitIso_inv_assoc, ← G.map_comp]
       rw [ι_colimMap])
 
 end
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Yoneda.lean b/Mathlib/CategoryTheory/Limits/Preserves/Yoneda.lean
index e0da3d65a8d90..dabe16ad73949 100644
--- a/Mathlib/CategoryTheory/Limits/Preserves/Yoneda.lean
+++ b/Mathlib/CategoryTheory/Limits/Preserves/Yoneda.lean
@@ -61,7 +61,7 @@ theorem yonedaYonedaColimit_app_inv {X : C} : ((yonedaYonedaColimit F).app (op X
   intro j
   rw [colimit.ι_post, ι_colimMap_assoc]
   simp only [← CategoryTheory.Functor.assoc, comp_evaluation]
-  rw [ι_preservesColimitsIso_inv_assoc, ← Functor.map_comp_assoc]
+  rw [ι_preservesColimitIso_inv_assoc, ← Functor.map_comp_assoc]
   simp only [← comp_evaluation]
   rw [colimitObjIsoColimitCompEvaluation_ι_inv, whiskerLeft_app]
   ext η Y f
diff --git a/Mathlib/Geometry/Manifold/Sheaf/Smooth.lean b/Mathlib/Geometry/Manifold/Sheaf/Smooth.lean
index 6cc1c879d0531..1bb560ec583ab 100644
--- a/Mathlib/Geometry/Manifold/Sheaf/Smooth.lean
+++ b/Mathlib/Geometry/Manifold/Sheaf/Smooth.lean
@@ -298,7 +298,7 @@ def smoothSheafCommRing.forgetStalk (x : TopCat.of M) :
         (colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U))
       (forgetStalk IM I M R x).hom =
     colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M R).presheaf) U :=
-  ι_preservesColimitsIso_hom _ _ _
+  ι_preservesColimitIso_hom _ _ _
 
 @[simp, reassoc, elementwise] lemma smoothSheafCommRing.ι_forgetStalk_inv (x : TopCat.of M) (U) :
     colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M R).presheaf) U ≫
diff --git a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean
index f549a8e9ee841..6befd6aab6a80 100644
--- a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean
+++ b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean
@@ -688,7 +688,7 @@ instance sheafedSpace_hasPullback_of_right : HasPullback g f :=
 instance sheafedSpace_pullback_snd_of_left :
     SheafedSpace.IsOpenImmersion (pullback.snd f g) := by
   delta pullback.snd
-  have : _ = limit.π (cospan f g) right := preservesLimitsIso_hom_π forget (cospan f g) right
+  have : _ = limit.π (cospan f g) right := preservesLimitIso_hom_π forget (cospan f g) right
   rw [← this]
   have := HasLimit.isoOfNatIso_hom_π (diagramIsoCospan (cospan f g ⋙ forget)) right
   erw [Category.comp_id] at this
@@ -699,7 +699,7 @@ instance sheafedSpace_pullback_snd_of_left :
 instance sheafedSpace_pullback_fst_of_right :
     SheafedSpace.IsOpenImmersion (pullback.fst g f) := by
   delta pullback.fst
-  have : _ = limit.π (cospan g f) left := preservesLimitsIso_hom_π forget (cospan g f) left
+  have : _ = limit.π (cospan g f) left := preservesLimitIso_hom_π forget (cospan g f) left
   rw [← this]
   have := HasLimit.isoOfNatIso_hom_π (diagramIsoCospan (cospan g f ⋙ forget)) left
   erw [Category.comp_id] at this
@@ -840,7 +840,7 @@ variable [HasLimits C] {ι : Type v} (F : Discrete ι ⥤ SheafedSpace.{_, v, v}
   (i : Discrete ι)
 
 theorem sigma_ι_isOpenEmbedding : IsOpenEmbedding (colimit.ι F i).base := by
-  rw [← show _ = (colimit.ι F i).base from ι_preservesColimitsIso_inv (SheafedSpace.forget C) F i]
+  rw [← show _ = (colimit.ι F i).base from ι_preservesColimitIso_inv (SheafedSpace.forget C) F i]
   have : _ = _ ≫ colimit.ι (Discrete.functor ((F ⋙ SheafedSpace.forget C).obj ∘ Discrete.mk)) i :=
     HasColimit.isoOfNatIso_ι_hom Discrete.natIsoFunctor i
   rw [← Iso.eq_comp_inv] at this
@@ -871,12 +871,12 @@ theorem image_preimage_is_empty (j : Discrete ι) (h : i ≠ j) (U : Opens (F.ob
   replace eq := ConcreteCategory.congr_arg (preservesColimitIso (SheafedSpace.forget C) F ≪≫
     HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫ TopCat.sigmaIsoSigma.{v, v} _).hom eq
   simp_rw [CategoryTheory.Iso.trans_hom, ← TopCat.comp_app, ← PresheafedSpace.comp_base] at eq
-  rw [ι_preservesColimitsIso_inv] at eq
+  rw [ι_preservesColimitIso_inv] at eq
   change
     ((SheafedSpace.forget C).map (colimit.ι F i) ≫ _) y =
       ((SheafedSpace.forget C).map (colimit.ι F j) ≫ _) x at eq
   cases i; cases j
-  rw [ι_preservesColimitsIso_hom_assoc, ι_preservesColimitsIso_hom_assoc,
+  rw [ι_preservesColimitIso_hom_assoc, ι_preservesColimitIso_hom_assoc,
     HasColimit.isoOfNatIso_ι_hom_assoc, HasColimit.isoOfNatIso_ι_hom_assoc,
     TopCat.sigmaIsoSigma_hom_ι, TopCat.sigmaIsoSigma_hom_ι] at eq
   exact h (congr_arg Discrete.mk (congr_arg Sigma.fst eq))
@@ -886,7 +886,7 @@ instance sigma_ι_isOpenImmersion [HasStrictTerminalObjects C] :
   base_open := sigma_ι_isOpenEmbedding F i
   c_iso U := by
     have e : colimit.ι F i = _ :=
-      (ι_preservesColimitsIso_inv SheafedSpace.forgetToPresheafedSpace F i).symm
+      (ι_preservesColimitIso_inv SheafedSpace.forgetToPresheafedSpace F i).symm
     have H :
       IsOpenEmbedding
         (colimit.ι (F ⋙ SheafedSpace.forgetToPresheafedSpace) i ≫
diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean
index 9b2339708fe4b..6f94368b8f4a6 100644
--- a/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean
+++ b/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean
@@ -307,7 +307,7 @@ def colimitPresheafObjIsoComponentwiseLimit (F : J ⥤ PresheafedSpace.{_, _, v}
     refine congr_arg (Set.preimage · U.1) (funext fun x => ?_)
     erw [← TopCat.comp_app]
     congr
-    exact ι_preservesColimitsIso_inv (forget C) F (unop X)
+    exact ι_preservesColimitIso_inv (forget C) F (unop X)
   · intro X Y f
     change ((F.map f.unop).c.app _ ≫ _ ≫ _) ≫ (F.obj (unop Y)).presheaf.map _ = _ ≫ _
     rw [TopCat.Presheaf.Pushforward.comp_inv_app]
diff --git a/Mathlib/Topology/Gluing.lean b/Mathlib/Topology/Gluing.lean
index 87c5a52e0a494..644c93f2a65fb 100644
--- a/Mathlib/Topology/Gluing.lean
+++ b/Mathlib/Topology/Gluing.lean
@@ -166,7 +166,7 @@ theorem eqvGen_of_π_eq
   let diagram := parallelPair 𝖣.diagram.fstSigmaMap 𝖣.diagram.sndSigmaMap ⋙ forget _
   have : colimit.ι diagram one x = colimit.ι diagram one y := by
     dsimp only [coequalizer.π, ContinuousMap.toFun_eq_coe] at h
-    rw [← ι_preservesColimitsIso_hom, forget_map_eq_coe, types_comp_apply, h]
+    rw [← ι_preservesColimitIso_hom, forget_map_eq_coe, types_comp_apply, h]
     simp
   have :
     (colimit.ι diagram _ ≫ colim.map _ ≫ (colimit.isoColimitCocone _).hom) _ =