∀ {R : Type u_1} [inst : CommRing R] (X : CoalgCat R),
  ModuleCat.Hom.hom
      (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom CoalgebraStruct.comul)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (ModuleCat.of R ↑X.toModuleCat)
          (ModuleCat.ofHom CoalgebraStruct.counit))) =
    ModuleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor (ModuleCat.of R ↑X.toModuleCat)).inv