∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v', u'} D] [inst_1 : CategoryTheory.MonoidalCategory D]
  (f : C → D) (x x_1 : CategoryTheory.FreeMonoidalCategory C) (x_2 : x.Hom x_1),
  CategoryTheory.FreeMonoidalCategory.projectMapAux f x_2 =
    match x, x_1, x_2 with
    | x, .(x), CategoryTheory.FreeMonoidalCategory.Hom.id .(x) =>
      CategoryTheory.CategoryStruct.id (CategoryTheory.FreeMonoidalCategory.projectObj f x)
    | .((X.tensor Y).tensor Z), .(X.tensor (Y.tensor Z)), 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
    | .(X.tensor (Y.tensor Z)), .((X.tensor Y).tensor Z), CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z =>
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.FreeMonoidalCategory.projectObj f X)
          (CategoryTheory.FreeMonoidalCategory.projectObj f Y) (CategoryTheory.FreeMonoidalCategory.projectObj f Z)).inv
    | .(CategoryTheory.FreeMonoidalCategory.unit.tensor a), a, CategoryTheory.FreeMonoidalCategory.Hom.l_hom .(a) =>
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.FreeMonoidalCategory.projectObj f a)).hom
    | a, .(CategoryTheory.FreeMonoidalCategory.unit.tensor a), CategoryTheory.FreeMonoidalCategory.Hom.l_inv .(a) =>
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.FreeMonoidalCategory.projectObj f a)).inv
    | .(a.tensor CategoryTheory.FreeMonoidalCategory.unit), a, CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom .(a) =>
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.FreeMonoidalCategory.projectObj f a)).hom
    | a, .(a.tensor CategoryTheory.FreeMonoidalCategory.unit), CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv .(a) =>
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.FreeMonoidalCategory.projectObj f a)).inv
    | x, x_3, f_1.comp g =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeMonoidalCategory.projectMapAux f f_1)
        (CategoryTheory.FreeMonoidalCategory.projectMapAux f g)
    | .(X.tensor Y₁), .(X.tensor Y₂), CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X p =>
      CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.FreeMonoidalCategory.projectObj f X)
        (CategoryTheory.FreeMonoidalCategory.projectMapAux f p)
    | .(X₁.tensor X), .(X₂.tensor X), p.whiskerRight X =>
      CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.FreeMonoidalCategory.projectMapAux f p)
        (CategoryTheory.FreeMonoidalCategory.projectObj f X)
    | .(W.tensor X), .(Y.tensor Z), f_1.tensor g =>
      CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.FreeMonoidalCategory.projectMapAux f f_1)
        (CategoryTheory.FreeMonoidalCategory.projectMapAux f g)