∀ {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)
  [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 :
    ∀ {X S : C} (πX : X ⟶ S),
      CategoryTheory.Limits.HasColimitsOfShape
        (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C]
  {π₁ π₂ π₃ : CategoryTheory.Arrow C} (τ : π₁ ⟶ π₂) (τ' : π₂ ⟶ π₃),
  CategoryTheory.Arrow.homMk (CategoryTheory.SmallObject.functorMap f (CategoryTheory.CategoryStruct.comp τ τ'))
      (CategoryTheory.CategoryStruct.comp τ τ').right ⋯ =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Arrow.homMk (CategoryTheory.SmallObject.functorMap f τ) τ.right ⋯)
      (CategoryTheory.Arrow.homMk (CategoryTheory.SmallObject.functorMap f τ') τ'.right ⋯)