∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {D : Type u_6}
  [inst_1 : CategoryTheory.Category.{u_5, u_6} D] {F : CategoryTheory.Functor D C} {J : Type u_2}
  [inst_2 : CategoryTheory.Category.{u_1, u_2} J] {R : CategoryTheory.Functor J F.PartialLeftAdjointSource}
  {c : CategoryTheory.Limits.Cocone (R.comp F.leftAdjointObjIsDefined.ι)}
  {c' : CategoryTheory.Limits.Cocone (R.comp F.partialLeftAdjoint)} (hc' : CategoryTheory.Limits.IsColimit c') {Y : D}
  (g : (F.comp (CategoryTheory.coyoneda.obj (Opposite.op c.pt))).obj Y) (j j' : J) (φ : j ⟶ j'),
  CategoryTheory.CategoryStruct.comp ((R.comp F.leftAdjointObjIsDefined.ι).map φ)
      (F.partialLeftAdjointHomEquiv
        (CategoryTheory.CategoryStruct.comp (c'.ι.app j')
          (hc'.desc
            { pt := Y,
              ι :=
                { app := fun j => F.partialLeftAdjointHomEquiv.symm (CategoryTheory.CategoryStruct.comp (c.ι.app j) g),
                  naturality := ⋯ } }))) =
    CategoryTheory.CategoryStruct.comp
      (F.partialLeftAdjointHomEquiv
        (CategoryTheory.CategoryStruct.comp (c'.ι.app j)
          (hc'.desc
            { pt := Y,
              ι :=
                { app := fun j => F.partialLeftAdjointHomEquiv.symm (CategoryTheory.CategoryStruct.comp (c.ι.app j) g),
                  naturality := ⋯ } })))
      (((CategoryTheory.Functor.const J).obj (F.1 Y)).map φ)