∀ {I : Type u_2} {C : I → Type u_3} [inst : (i : I) → CategoryTheory.Category.{u_1, u_3} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : I → Type u_5}
  [inst_2 : (i : I) → CategoryTheory.Category.{u_4, u_5} (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 : (i : I) → D i),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor ((CategoryTheory.Functor.pi F).obj X)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((CategoryTheory.Functor.pi F).obj X) fun i =>
        CategoryTheory.Functor.LaxMonoidal.ε (F i))
      (CategoryTheory.CategoryStruct.comp
        (fun i =>
          CategoryTheory.Functor.LaxMonoidal.μ (F i) (X i)
            (CategoryTheory.MonoidalCategoryStruct.tensorUnit ((i : I) → D i) i))
        ((CategoryTheory.Functor.pi F).map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom))