∀ {I : Type u_2} {C : I → Type u_5} [inst : (i : I) → CategoryTheory.Category.{u_4, u_5} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : I → Type u_3}
  [inst_2 : (i : I) → CategoryTheory.Category.{u_1, u_3} (D i)]
  [inst_3 : (i : I) → CategoryTheory.MonoidalCategory (D i)] (F : (i : I) → CategoryTheory.Functor (D i) (C i))
  [inst_4 : (i : I) → (F i).LaxMonoidal] {X Y : (i : I) → D i} (X' : (i : I) → D i) (f : X ⟶ Y),
  (CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((CategoryTheory.Functor.pi F).obj X')
        ((CategoryTheory.Functor.pi F).map f))
      fun i => CategoryTheory.Functor.LaxMonoidal.μ (F i) (X' i) (Y i)) =
    CategoryTheory.CategoryStruct.comp (fun i => CategoryTheory.Functor.LaxMonoidal.μ (F i) (X' i) (X i))
      ((CategoryTheory.Functor.pi F).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' f))