∀ {J : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} J] {ι : Type u_3} {j : J} {k : ι → J}
  (f : (i : ι) → j ⟶ k i) (l : J) (hl : ∀ (i : ι), Nonempty (k i ⟶ l)) (m : J) (b : l ⟶ m) (c : j ⟶ m),
  (∀ (i : ι),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (f i) ((fun i => ⋯.some) i)) b = c) →
    ∀ (i : ι), CategoryTheory.CategoryStruct.comp (f i) (CategoryTheory.CategoryStruct.comp ((fun i => ⋯.some) i) b) = c