∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] [inst_2 : UniformSpace G]
  [hG : IsUniformAddGroup G] [inst_3 : UniformSpace H] [hH : IsUniformAddGroup H], IsUniformAddGroup (G × H)