∀ (C : Type u_3) {D : Type u_5} {E : Type u_1} [inst : CategoryTheory.Category.{u_2, u_3} C]
  [inst_1 : CategoryTheory.Category.{u_6, u_5} D] [inst_2 : CategoryTheory.Category.{u_4, u_1} E]
  {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} (adj : F ⊣ G) (X : CategoryTheory.Functor D C),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Functor.whiskeringLeft E D C).obj G).map
        ({
              app := fun X =>
                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),
              naturality := ⋯ }.app
          X))
      ({
            app := fun X =>
              CategoryTheory.CategoryStruct.comp (G.associator F X).inv
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight adj.counit X)
                  X.leftUnitor.hom),
            naturality := ⋯ }.app
        (((CategoryTheory.Functor.whiskeringLeft E D C).obj G).obj X)) =
    CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.whiskeringLeft E D C).obj G).obj X)