∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {ι : Type u_4} {S : C} {X : ι → C}
  {f : (i : ι) → X i ⟶ S} {ι' : Type u_3} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} ⦃W : C⦄ (q : W ⟶ S) ⦃i₁ : ι⦄
  (f₁ : W ⟶ X i₁),
  CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q →
    ∀ (j : ι') (T : C) (g : T ⟶ X' j) (p : T ⟶ W),
      CategoryTheory.CategoryStruct.comp g (f' j) = CategoryTheory.CategoryStruct.comp p q →
        CategoryTheory.CategoryStruct.comp g (f' j) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp p f₁) (f i₁)