English
If for every pair A, B the component prodComparison F A B is an isomorphism, then the bifunctorial natural transformation prodComparisonNatTrans F is an isomorphism.
Русский
Если для каждого пары объектов A, B компонент prodComparison F A B является изоморфизмом, то бифункторное натуральное преобразование prodComparisonNatTrans F тоже является изоморфизмом.
LaTeX
$$$\big( \forall A,B, \text{IsIso}(\mathrm{prodComparison}\, F\, A\, B) \big) \Rightarrow \mathrm{IsIso}(\mathrm{prodComparisonNatTrans}\, F)$$
Lean4
instance (A : C) [∀ B, IsIso (prodComparison F A B)] : IsIso (prodComparisonNatTrans F A) :=
by
letI : ∀ X, IsIso ((prodComparisonNatTrans F A).app X) := by assumption
apply NatIso.isIso_of_isIso_app
