English
If prodComparison F A B is an isomorphism for all A,B, then prodComparisonNatTrans F is an isomorphism.
Русский
Если для всех A,B лав prodComparison F A B является изоморфизмом, то prodComparisonNatTrans F является изоморфизмом.
LaTeX
$$$\forall A,B\,IsIso(\mathrm{prodComparison}\, F\, A\, B) \Rightarrow IsIso(\mathrm{prodComparisonNatTrans}\, F)$$$
Lean4
instance [∀ A B, IsIso (prodComparison F A B)] : IsIso (prodComparisonBifunctorNatTrans F) :=
by
letI : ∀ X, IsIso ((prodComparisonBifunctorNatTrans F).app X) := fun _ ↦ by dsimp; apply NatIso.isIso_of_isIso_app
apply NatIso.isIso_of_isIso_app
