From 1c924dae1162c39e97f58643215e40f6b8f24213 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Sun, 23 Feb 2025 15:56:56 +0000 Subject: [PATCH] chore(CategoryTheory): fix incorrect name (#22210) Co-authored-by: Markus Himmel --- .../Limits/FunctorCategory/Shapes/Products.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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