∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (M : CategoryTheory.Comonad C) (X : C),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.id M.toFunctor).app X) (M.δ.app X) =
    CategoryTheory.CategoryStruct.comp (M.δ.app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.id M.toFunctor).app (M.obj X))
        (M.map ((CategoryTheory.CategoryStruct.id M.toFunctor).app X)))