∀ (C : Type u_4) {D : Type u_3} {E : Type u_5} [inst : CategoryTheory.Category.{u_2, u_4} C]
  [inst_1 : CategoryTheory.Category.{u_1, u_3} D] [inst_2 : CategoryTheory.Category.{u_6, u_5} E]
  {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} (adj : F ⊣ G) ⦃X Y : CategoryTheory.Functor D C⦄
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.id (CategoryTheory.Functor D C)).map f)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.id (CategoryTheory.Functor D C)).obj Y).leftUnitor.inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight adj.unit Y) (F.associator G Y).hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.id (CategoryTheory.Functor D C)).obj X).leftUnitor.inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight adj.unit X) (F.associator G X).hom))
      ((((CategoryTheory.Functor.whiskeringLeft E D C).obj G).comp
            ((CategoryTheory.Functor.whiskeringLeft D E C).obj F)).map
        f)