∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y : C) ⦃X_1 Y_1 : CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)⦄ (f : X_1 ⟶ Y_1),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.id (CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))).map f)
      (CategoryTheory.Over.homMk
        (CategoryTheory.CartesianMonoidalCategory.lift
          (CategoryTheory.CategoryStruct.comp Y_1.hom (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y))
          (CategoryTheory.CategoryStruct.id
            ((CategoryTheory.Functor.id (CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))).obj
                Y_1).left))
        ⋯) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.homMk
        (CategoryTheory.CartesianMonoidalCategory.lift
          (CategoryTheory.CategoryStruct.comp X_1.hom (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y))
          (CategoryTheory.CategoryStruct.id
            ((CategoryTheory.Functor.id (CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))).obj
                X_1).left))
        ⋯)
      (((CategoryTheory.Over.map (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)).comp
            { obj := fun Z => CategoryTheory.Over.mk (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X Z.hom),
              map := fun {X_2 Y_2} g =>
                CategoryTheory.Over.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g.left) ⋯,
              map_id := ⋯, map_comp := ⋯ }).map
        f)