∀ {M : Type u_1} [inst : AddMonoid M] {N : Type u_2} [inst_1 : AddMonoid N] (F : M →+ N)
  (X Y Z : CategoryTheory.Discrete M),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Discrete.eqToIso ⋯).hom
        ((CategoryTheory.Discrete.addMonoidalFunctor F).obj Z))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Discrete.eqToIso ⋯).hom
        ((CategoryTheory.Discrete.addMonoidalFunctor F).map
          (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator ((CategoryTheory.Discrete.addMonoidalFunctor F).obj X)
          ((CategoryTheory.Discrete.addMonoidalFunctor F).obj Y)
          ((CategoryTheory.Discrete.addMonoidalFunctor F).obj Z)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((CategoryTheory.Discrete.addMonoidalFunctor F).obj X)
          (CategoryTheory.Discrete.eqToIso ⋯).hom)
        (CategoryTheory.Discrete.eqToIso ⋯).hom)