chore(Geometry/RingedSpace/PresheafedSpace/HasColimits): remove an erw (#38506)

- rewrites the `TopCat.comp_app` step in `colimitPresheafObjIsoComponentwiseLimit` with `simp only [colimitCocone, colimit, ← TopCat.comp_app]`
- folds `colimitCocone_ι_app_c`, `limitObjIsoLimitCompEvaluation_inv_π_app_assoc`, and `limMap_π_assoc` into a single `rw` chain in `colimitPresheafObjIsoComponentwiseLimit_inv_ι_app`

Extracted from #38415

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

Author: yuanyi-350

Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean

@@ -304,7 +304,7 @@ def colimitPresheafObjIsoComponentwiseLimit (F : J ⥤ PresheafedSpace.{_, _, v}
     simp only [Functor.op_obj, op_inj_iff, Opens.map_coe, SetLike.ext'_iff,
       Set.preimage_preimage]
     refine congr_arg (Set.preimage · U.1) (funext fun x => ?_)
-    erw [← TopCat.comp_app]
+    simp only [colimitCocone, colimit, ← TopCat.comp_app]
     congr
     exact ι_preservesColimitIso_inv (forget C) F (unop X)
   · intro X Y f
@@ -327,9 +327,8 @@ theorem colimitPresheafObjIsoComponentwiseLimit_inv_ι_app (F : J ⥤ Presheafed
     congr_app (Iso.symm_inv _)]
   dsimp
   rw [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality,
-      ← comp_c_app_assoc,
-      congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc]
-  erw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc]
+      ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc,
+      colimitCocone_ι_app_c, limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc]
   simp
 
 set_option backward.isDefEq.respectTransparency false in