From 90dd5725e9ef001b02728fc9d2b6df84ea3c2dda Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Sat, 25 Apr 2026 15:48:52 +0800 Subject: [PATCH] chore(Geometry/RingedSpace/PresheafedSpace/HasColimits): remove an erw --- .../Geometry/RingedSpace/PresheafedSpace/HasColimits.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) 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