diff --git a/Mathlib/CategoryTheory/Limits/ColimitLimit.lean b/Mathlib/CategoryTheory/Limits/ColimitLimit.lean
index b399182aff4d69..fdf3e279207679 100644
--- a/Mathlib/CategoryTheory/Limits/ColimitLimit.lean
+++ b/Mathlib/CategoryTheory/Limits/ColimitLimit.lean
@@ -111,6 +111,6 @@ noncomputable def colimitLimitToLimitColimitCone (G : J ⥤ K ⥤ C) [HasLimit G
       ι_colimitLimitToLimitColimit_π_assoc, curry_obj_obj_obj, Prod.swap_obj,
       uncurry_obj_obj, ι_colimMap, currying_unitIso_inv_app_app_app, Category.id_comp,
       limMap_π_assoc, Functor.flip_obj_obj, flipIsoCurrySwapUncurry_hom_app_app]
-    erw [limitObjIsoLimitCompEvaluation_hom_π_assoc]
+    simp only [← comp_evaluation G k, limitObjIsoLimitCompEvaluation_hom_π_assoc]
 
 end CategoryTheory.Limits