English
If G and H have TwoUniqueProds, then G × H has TwoUniqueProds.
Русский
Если G и H обладают TwoUniqueProds, то их произведение G × H обладает TwoUniqueProds.
LaTeX
$$$ \\forall G,H\\,[\\mathrm{Mul }G][\\mathrm{Mul }H] [\\mathrm{TwoUniqueProds }G][\\mathrm{TwoUniqueProds }H] \\Rightarrow \\mathrm{TwoUniqueProds}(G \\times H). $$$
Lean4
@[to_additive]
instance _root_.Prod.instTwoUniqueProds [TwoUniqueProds G] [TwoUniqueProds H] : TwoUniqueProds (G × H) :=
by
have : ∀ b, TwoUniqueProds (I G H b) := Bool.rec ?_ ?_
· exact of_injective_mulHom (downMulHom H) down_injective ‹_›
· refine
of_injective_mulHom (Prod.upMulHom G H) (fun x y he ↦ Prod.ext ?_ ?_) (TwoUniqueProds.instForall <| I G H) <;>
apply up_injective
exacts [congr_fun he false, congr_fun he true]
· exact of_injective_mulHom (downMulHom G) down_injective ‹_›
