∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.Limits.HasFiniteColimits C]
  (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [inst_2 : CategoryTheory.SmallCategory J]
  [inst_3 : CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J Cᵒᵖ)
  [inst_4 : CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)],
  (CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso A K).hom =
    CategoryTheory.Limits.limit.post K A