∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X : C} (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (X_1 : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Over.map f).map
        ({
              app := fun T =>
                CategoryTheory.Over.homMk
                  (CategoryTheory.CartesianMonoidalCategory.lift
                    (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id (CategoryTheory.Over X)).obj T).left)
                    T.hom)
                  ⋯,
              naturality := ⋯ }.app
          X_1))
      ({ app := fun U => CategoryTheory.Over.homMk (CategoryTheory.SemiCartesianMonoidalCategory.fst U.left X) ⋯,
            naturality := ⋯ }.app
        ((CategoryTheory.Over.map f).obj X_1)) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Over.map f).obj X_1)