chore(CategoryTheory/Limits/ColimitLimit): remove an erw (#38518)

- adds `← comp_evaluation G k` to the simplification step, so `limitObjIsoLimitCompEvaluation_hom_π_assoc` no longer needs `erw`

Extracted from #38415

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author: yuanyi-350

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