∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{w', u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) {A B : C} [inst_3 : CategoryTheory.Limits.HasBinaryProduct A B]
  [inst_4 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)]
  [inst_5 : CategoryTheory.Limits.HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))]
  [inst_6 : CategoryTheory.Limits.HasBinaryProduct ((F.comp G).obj A) ((F.comp G).obj B)],
  CategoryTheory.Limits.prodComparison (F.comp G) A B =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.prodComparison F A B))
      (CategoryTheory.Limits.prodComparison G (F.obj A) (F.obj B))