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