no goals
C : Type u
inst✝⁵ : Category C
X Y : C
D : Type u₂
inst✝⁴ : Category D
F : C ⥤ D
A A' B B' : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct A' B'
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ F.map (prod.map f g) ≫ prodComparison F A' B' = prodComparison F A B ≫ prod.map (F.map f) (F.map g)
rw [prodComparison, prodComparison, prod.lift_map, ← F.map_comp, ← F.map_comp, prod.comp_lift, ←
  F.map_comp, prod.map_fst, ← F.map_comp, prod.map_snd]