∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : CategoryTheory.Mon C) {M_1 N : Cᵒᵖ} (φ : M_1 ⟶ N),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.yonedaMonObj M.X).map φ)
      (MonCat.ofHom
        { toFun := fun x => CategoryTheory.CategoryStruct.comp x (CategoryTheory.CategoryStruct.id M).hom,
          map_one' := ⋯, map_mul' := ⋯ }) =
    CategoryTheory.CategoryStruct.comp
      (MonCat.ofHom
        { toFun := fun x => CategoryTheory.CategoryStruct.comp x (CategoryTheory.CategoryStruct.id M).hom,
          map_one' := ⋯, map_mul' := ⋯ })
      ((CategoryTheory.yonedaMonObj M.X).map φ)