theorem ProductGroups.prod_group_mul_def {G : Type u_1} {H : Type u_2} [Group G] [Group H] (g₁ g₂ : G) (h₁ h₂ : H) : (g₁, h₁) * (g₂, h₂) = (g₁ * g₂, h₁ * h₂)