∀ {C : Type u_1} {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.FreeMonoidalCategory C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂)
  (f₃ : X₃ ⟶ Y₃),
  CategoryTheory.CategoryStruct.comp
      (Quotient.map₂ CategoryTheory.FreeMonoidalCategory.Hom.tensor ⋯
        (Quotient.map₂ CategoryTheory.FreeMonoidalCategory.Hom.tensor ⋯ f₁ f₂) f₃)
      { hom := ⟦CategoryTheory.FreeMonoidalCategory.Hom.α_hom Y₁ Y₂ Y₃⟧,
          inv := ⟦CategoryTheory.FreeMonoidalCategory.Hom.α_inv Y₁ Y₂ Y₃⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
    CategoryTheory.CategoryStruct.comp
      { hom := ⟦CategoryTheory.FreeMonoidalCategory.Hom.α_hom X₁ X₂ X₃⟧,
          inv := ⟦CategoryTheory.FreeMonoidalCategory.Hom.α_inv X₁ X₂ X₃⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom
      (Quotient.map₂ CategoryTheory.FreeMonoidalCategory.Hom.tensor ⋯ f₁
        (Quotient.map₂ CategoryTheory.FreeMonoidalCategory.Hom.tensor ⋯ f₂ f₃))