no goals
C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category C
inst✝¹ : Category D
inst✝ : Category E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map (𝟙 X, g) ≫ F.map (f, 𝟙 Y') = F.map (f, g)
rw [← Functor.map_comp, prod_comp, Category.id_comp, Category.comp_id]