∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v', u'} D] [inst_1 : CategoryTheory.MonoidalCategory D]
  (f : C → D) (X Y Z : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.projectMapAux f (CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z) =
    (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.FreeMonoidalCategory.projectObj f X)
        (CategoryTheory.FreeMonoidalCategory.projectObj f Y) (CategoryTheory.FreeMonoidalCategory.projectObj f Z)).hom