∀ {T : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} T] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{u_1, u_2} D] {Y : D} {F : CategoryTheory.Functor T D}
  {G : CategoryTheory.Functor D T} (a : F ⊣ G) (A : CategoryTheory.Over ((CategoryTheory.Functor.id D).obj Y)),
  CategoryTheory.CategoryStruct.comp (a.counit.app A.left)
      ((CategoryTheory.Functor.id (CategoryTheory.Over ((CategoryTheory.Functor.id D).obj Y))).obj A).hom =
    (((CategoryTheory.Over.post G).comp
            ((CategoryTheory.Over.post F).comp (CategoryTheory.Over.map (a.counit.app Y)))).obj
        A).hom