∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {I : Type u_3} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY)
  (x : CategoryTheory.SmallObject.FunctorObjIndex f πX),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp x.t τ.left) πY =
    CategoryTheory.CategoryStruct.comp (f x.i) (CategoryTheory.CategoryStruct.comp x.b τ.right)