∀ {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 Y⦄ (f : X_1 ⟶ Y_1),
  CategoryTheory.CategoryStruct.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 := ⋯ }.comp
            (CategoryTheory.Over.map (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y))).map
        f)
      (CategoryTheory.Over.homMk
        (CategoryTheory.SemiCartesianMonoidalCategory.snd X ((CategoryTheory.Functor.id C).obj Y_1.left)) ⋯) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.homMk
        (CategoryTheory.SemiCartesianMonoidalCategory.snd X ((CategoryTheory.Functor.id C).obj X_1.left)) ⋯)
      ((CategoryTheory.Functor.id (CategoryTheory.Over Y)).map f)