From 59a74f9085d80f05a99adbc9cceb0bde8f05d30a Mon Sep 17 00:00:00 2001
From: euprunin <euprunin@users.noreply.github.com>
Date: Sun, 7 Dec 2025 17:47:04 +0100
Subject: [PATCH] chore(CategoryTheory/Limits): remove use of `erw` in
 `prod_preservesConnectedLimits`

---
 Mathlib/CategoryTheory/Limits/Connected.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Limits/Connected.lean b/Mathlib/CategoryTheory/Limits/Connected.lean
index 2cdafc463942cb..b00864b73e0b8d 100644
--- a/Mathlib/CategoryTheory/Limits/Connected.lean
+++ b/Mathlib/CategoryTheory/Limits/Connected.lean
@@ -226,8 +226,7 @@ lemma prod_preservesConnectedLimits [IsConnected J] (X : C) :
             · simp
           uniq := fun s m L => by
             apply Limits.prod.hom_ext
-            · erw [limit.lift_π, ← L (Classical.arbitrary J), assoc, limMap_π, comp_id]
-              rfl
+            · simp [← L]
             · rw [limit.lift_π]
               apply l.uniq (forgetCone s)
               intro j