∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.ComonObj X],
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ComonObj.counit X) =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv