∀ {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)] {X Y : (i : I) → C i} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit ((i : I) → C i)) f)
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom f