∀ {C : Type u_1} {D : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} D]
  [inst_1 : CategoryTheory.MonoidalCategory D] (f : C → D) (X Y Z : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.Iso.refl
            (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.FreeMonoidalCategory.project f).obj X)
              ((CategoryTheory.FreeMonoidalCategory.project f).obj Y))).hom
        ((CategoryTheory.FreeMonoidalCategory.project f).obj Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Iso.refl
            (CategoryTheory.MonoidalCategoryStruct.tensorObj
              ((CategoryTheory.FreeMonoidalCategory.project f).obj
                (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
              ((CategoryTheory.FreeMonoidalCategory.project f).obj Z))).hom
        ((CategoryTheory.FreeMonoidalCategory.project f).map
          (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator ((CategoryTheory.FreeMonoidalCategory.project f).obj X)
          ((CategoryTheory.FreeMonoidalCategory.project f).obj Y)
          ((CategoryTheory.FreeMonoidalCategory.project f).obj Z)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((CategoryTheory.FreeMonoidalCategory.project f).obj X)
          (CategoryTheory.Iso.refl
              (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.FreeMonoidalCategory.project f).obj Y)
                ((CategoryTheory.FreeMonoidalCategory.project f).obj Z))).hom)
        (CategoryTheory.Iso.refl
            (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.FreeMonoidalCategory.project f).obj X)
              ((CategoryTheory.FreeMonoidalCategory.project f).obj
                (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)))).hom)