∀ {I : Type u_2} {C : I → Type u_3} [inst : (i : I) → CategoryTheory.Category.{u_1, u_3} (C i)] {E : Type u_5}
  [inst_1 : CategoryTheory.Category.{u_4, u_5} E] {F G : CategoryTheory.Functor E ((i : I) → C i)}
  (τ : (i : I) → F.comp (CategoryTheory.Pi.eval C i) ⟶ G.comp (CategoryTheory.Pi.eval C i)) (x x_1 : E) (f : x ⟶ x_1),
  (CategoryTheory.CategoryStruct.comp (F.map f) fun i => (τ i).app x_1) =
    CategoryTheory.CategoryStruct.comp (fun i => (τ i).app x) (G.map f)