∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {F : CategoryTheory.Functor T D} {G : CategoryTheory.Functor D T} (a : F ⊣ G)
  (A : CategoryTheory.Under (F.obj ((CategoryTheory.Functor.id T).obj X))),
  (CategoryTheory.Under.postAdjunctionLeft a).counit.app A = CategoryTheory.Under.homMk (a.counit.app A.right) ⋯