diff --git a/Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Products.lean b/Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Products.lean
index f05196a209fdc..b21f86509e1a5 100644
--- a/Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Products.lean
+++ b/Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Products.lean
@@ -36,10 +36,13 @@ theorem piObjIso_hom_comp_π (f : α → D ⥤ C) (d : D) (s : α) :
   simp [piObjIso]
 
 @[reassoc (attr := simp)]
-theorem piObjIso_inv_comp_pi (f : α → D ⥤ C) (d : D) (s : α) :
+theorem piObjIso_inv_comp_π (f : α → D ⥤ C) (d : D) (s : α) :
     (piObjIso f d).inv ≫ (Pi.π f s).app d = Pi.π (fun s => (f s).obj d) s := by
   simp [piObjIso]
 
+@[deprecated (since := "2025-02-23")]
+alias piObjIso_inv_comp_pi := piObjIso_inv_comp_π
+
 end Product
 
 section Coproduct