∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Comon C} (f : M.X ≅ N.X)
  (f_counit :
    autoParam (CategoryTheory.CategoryStruct.comp f.hom CategoryTheory.ComonObj.counit = CategoryTheory.ComonObj.counit)
      CategoryTheory.Comon.mkIso._auto_1)
  (f_comul :
    autoParam
      (CategoryTheory.CategoryStruct.comp f.hom CategoryTheory.ComonObj.comul =
        CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
          (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom))
      CategoryTheory.Comon.mkIso._auto_3),
  (CategoryTheory.Comon.mkIso f f_counit f_comul).inv.hom = f.inv