∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) (X : C)
  (a :
    (CategoryTheory.yoneda.comp
          (((CategoryTheory.Functor.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).obj F.op).comp CategoryTheory.Limits.lim)).obj
      X)
  (j : J),
  ((CategoryTheory.Limits.yonedaCompLimIsoCocones F).hom.app X a).app j =
    CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj X)) (Opposite.op j) a