∀ (R : Type u_1) [inst : CommRing R] {X Y : CoalgCat R} (x : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.id (CoalgCat R)).map x)
      ((fun x => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CoalgCat R)).obj x)) Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun x => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CoalgCat R)).obj x)) X).hom
      (((CoalgCat.toComon R).comp (CoalgCat.ofComon R)).map x)