∀ {I : Type u_3} {C : I → Type u_2} [inst : (i : I) → CategoryTheory.Category.{u_1, u_2} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] (i : I),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (C i)))
      (CategoryTheory.CategoryStruct.id
        ((CategoryTheory.Pi.eval C i).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit ((i : I) → C i)))) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (C i))