From 6029f2c8c91020b270455f4a60e4c23d6a831c93 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Sat, 25 Apr 2026 19:54:58 +0800 Subject: [PATCH] chore(CategoryTheory/Limits/ColimitLimit): remove an erw --- Mathlib/CategoryTheory/Limits/ColimitLimit.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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