chore(CategoryTheory): fix incorrect name (#22210)

Co-authored-by: Markus Himmel <[email protected]>
leanprover-community · Feb 23, 2025 · 1c924da · 1c924da
1 parent f7a295f
commit 1c924da
Showing 1 changed file with 4 additions and 1 deletion.
diff --git 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