∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ] {ι : Type v'} {j : J} {k : ι → J} (f : (i : ι) → j ⟶ k i),
  HasCardinalLT ι κ → ∃ m a b, ∀ (i : ι), CategoryTheory.CategoryStruct.comp (f i) (a i) = b