∀ {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) (i : I) {Z : Type u₂}
  (h : (CategoryTheory.yoneda.obj A).obj (Opposite.op (F.obj i)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda F A).inv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.yoneda.obj A).map (CategoryTheory.Limits.colimit.ι F i).op)
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj A)) (Opposite.op i)) h