∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X Y Z : CategoryTheory.Center C),
  X.associator Y Z =
    CategoryTheory.Center.isoMk
      { f := (CategoryTheory.MonoidalCategoryStruct.associator X.fst Y.fst Z.fst).hom, comm := ⋯ }