∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X Y : CategoryTheory.Center C),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Center.forget C) X Y =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Center.forget C).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))