∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor Iᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I (Type u₂)] (A : C),
  CategoryTheory.Limits.colimitHomIsoLimitYoneda' F A =
    (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda' F).app A ≪≫
      CategoryTheory.Limits.limitObjIsoLimitCompEvaluation (F.rightOp.comp CategoryTheory.coyoneda) A