∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {I : Type u_3} {Z Y : I → C} {X : C}
  (g : (i : I) → Z i ⟶ Y i) (f : (i : I) → Y i ⟶ X) {W : C} (φ : (a : I) → Y a ⟶ W) (m : X ⟶ W),
  (∀ (a : I), CategoryTheory.CategoryStruct.comp (f a) m = φ a) →
    ∀ (i : I),
      CategoryTheory.CategoryStruct.comp ((fun i => CategoryTheory.CategoryStruct.comp (g i) (f i)) i) m =
        CategoryTheory.CategoryStruct.comp (g i) (φ i)