diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean
index 8b1a3aadd2054f..c63842208ca42b 100644
--- a/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean
+++ b/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