∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (x : CategoryTheory.Endofunctor.Algebra F),
  CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Endofunctor.Algebra F)).obj x).a).hom)
      (((CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf adj).comp
              (CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf adj)).obj
          x).str =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.id (CategoryTheory.Endofunctor.Algebra F)).obj x).str
      (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Endofunctor.Algebra F)).obj x).a).hom