∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y : CategoryTheory.Comonad C} (x : X ⟶ Y) (X_1 : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (x.app X_1)
        ({ toNatTrans := CategoryTheory.CategoryStruct.id Y.toFunctor, app_ε := ⋯, app_δ := ⋯ }.app X_1))
      (Y.δ.app X_1) =
    CategoryTheory.CategoryStruct.comp (X.δ.app X_1)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CategoryStruct.comp (x.app (X.obj X_1))
          ({ toNatTrans := CategoryTheory.CategoryStruct.id Y.toFunctor, app_ε := ⋯, app_δ := ⋯ }.app (X.obj X_1)))
        (Y.map
          (CategoryTheory.CategoryStruct.comp (x.app X_1)
            ({ toNatTrans := CategoryTheory.CategoryStruct.id Y.toFunctor, app_ε := ⋯, app_δ := ⋯ }.app X_1))))