∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (D : Type u_4) [inst_2 : CategoryTheory.Category.{u_3, u_4} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {X Y Z : CategoryTheory.LaxMonoidalFunctor C D} (x : X ⟶ Y) (x_1 : Y ⟶ Z) ⦃X_1 Y_1 : CategoryTheory.Mon C⦄
  (f : X_1 ⟶ Y_1),
  CategoryTheory.CategoryStruct.comp (X.mapMon.map f)
      (CategoryTheory.Mon.Hom.mk' ((CategoryTheory.CategoryStruct.comp x x_1).hom.app Y_1.X) ⋯ ⋯) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Mon.Hom.mk' ((CategoryTheory.CategoryStruct.comp x x_1).hom.app X_1.X) ⋯ ⋯) (Z.mapMon.map f)