∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {I : Type u_1}
  [Finite I] {i : C} {j : I → C} (f : (x : I) → j x ⟶ i),
  ∃ k fki g, ∀ (x : I), CategoryTheory.CategoryStruct.comp (g x) (f x) = fki