∀ (M : Type u_1) [inst : CommMonoid M] (X Y Z : CategoryTheory.Discrete M),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Discrete.eqToIso ⋯).hom
        (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Discrete.eqToIso ⋯).hom Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Discrete.eqToIso ⋯).hom))