∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (D : CategoryTheory.Functor I Cᵒᵖ) (F : CategoryTheory.Functor C (Type u₂))
  [inst_2 : CategoryTheory.Limits.HasColimit (D.comp CategoryTheory.coyoneda)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))]
  (f : CategoryTheory.Limits.colimit (D.comp CategoryTheory.coyoneda) ⟶ F) (i : I),
  CategoryTheory.Limits.limit.π (D.leftOp.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂})) (Opposite.op i)
      ((CategoryTheory.Limits.colimitCoyonedaHomIsoLimitLeftOp D F).hom f) =
    {
      down :=
        f.app (Opposite.unop (D.obj i))
          ((CategoryTheory.Limits.colimit.ι (D.comp CategoryTheory.coyoneda) i).app (Opposite.unop (D.obj i))
            (CategoryTheory.CategoryStruct.id (Opposite.unop (D.obj i)))) }