∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (α : F ≅ G),
  (CategoryTheory.Endofunctor.Algebra.equivOfNatIso α).counitIso =
    (CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp α.inv α.hom).symm ≪≫
      CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq ⋯ ≪≫ CategoryTheory.Endofunctor.Algebra.functorOfNatTransId