∀ {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) (X : (i : I) → C i),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor ((CategoryTheory.Pi.eval C i).obj X)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((CategoryTheory.Pi.eval C i).obj X)
        (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (C i))))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CategoryStruct.id
          (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Pi.eval C i).obj X)
            ((CategoryTheory.Pi.eval C i).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit ((i : I) → C i)))))
        ((CategoryTheory.Pi.eval C i).map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom))