∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : C) [inst_2 : CategoryTheory.MonObj M] (X : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonObj.one X)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd M X) =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom