∀ {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] {X : T} {F : CategoryTheory.Functor T D}
  {G : CategoryTheory.Functor D T} (a : F ⊣ G)
  ⦃X_1 Y : CategoryTheory.Under (F.obj ((CategoryTheory.Functor.id T).obj X))⦄ (f : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ((((CategoryTheory.Under.post G).comp (CategoryTheory.Under.map (a.unit.app X))).comp
            (CategoryTheory.Under.post F)).map
        f)
      (CategoryTheory.Under.homMk (a.counit.app Y.right) ⋯) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.homMk (a.counit.app X_1.right) ⋯)
      ((CategoryTheory.Functor.id (CategoryTheory.Under (F.obj ((CategoryTheory.Functor.id T).obj X)))).map f)