English
Let f: A ⟶ A' and g: B ⟶ B'. If prodComparison is an isomorphism, then inv(prodComparison F A B) ≫ F.map (prod.map f g) = prod.map (F.map f) (F.map g) ≫ inv(prodComparison F A' B').
Русский
Пусть f: A→A', g: B→B'. При условии, что prodComparison является изоморфизмом, выполняется inv(prodComparison F A B) ∘ F.map(prod.map f g) = prod.map(F.map f)(F.map g) ∘ inv(prodComparison F A' B').
LaTeX
$$$ \\operatorname{inv}(\\operatorname{prodComparison} F A B) \\circ F\\big(\\operatorname{prod.map} f g\\big) = \\operatorname{prod.map}(F f)(F g) \\circ \\operatorname{inv}(\\operatorname{prodComparison} F A' B') $$$
Lean4
/-- Naturality of the `prodComparison` morphism in both arguments. -/
@[reassoc]
theorem prodComparison_natural (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) := by
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]
