∀ (C : Type u_3) {D : Type u_6} {E : Type u_4} [inst : CategoryTheory.Category.{u_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{u_5, u_6} D] [inst_2 : CategoryTheory.Category.{u_2, u_4} E]
  {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} (adj : F ⊣ G) (Y : CategoryTheory.Functor C E),
  CategoryTheory.CategoryStruct.comp
      ({
            app := fun X =>
              CategoryTheory.CategoryStruct.comp
                ((CategoryTheory.Functor.id (CategoryTheory.Functor C D)).obj X).rightUnitor.inv
                (CategoryTheory.CategoryStruct.comp (X.whiskerLeft adj.unit) (X.associator F G).inv),
            naturality := ⋯ }.app
        (((CategoryTheory.Functor.whiskeringRight C E D).obj G).obj Y))
      (((CategoryTheory.Functor.whiskeringRight C E D).obj G).map
        ({
              app := fun X =>
                CategoryTheory.CategoryStruct.comp (X.associator G F).hom
                  (CategoryTheory.CategoryStruct.comp (X.whiskerLeft adj.counit) X.rightUnitor.hom),
              naturality := ⋯ }.app
          Y)) =
    CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.whiskeringRight C E D).obj G).obj Y)