∀ {C : Type u_6} [inst : CategoryTheory.Category.{u_5, u_6} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {J : Type u_3} [inst_2 : CategoryTheory.Category.{u_1, u_3} J] (K : CategoryTheory.Functor J D)
  ⦃X Y : CategoryTheory.Limits.Cone K⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Limits.Cones.functoriality K G).comp (adj.functorialityLeftAdjoint K)).map f)
      { hom := adj.counit.app Y.pt, w := ⋯ } =
    CategoryTheory.CategoryStruct.comp { hom := adj.counit.app X.pt, w := ⋯ }
      ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone K)).map f)