∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [NonarchimedeanAddGroup G] {K : Type u_3}
  [inst_3 : AddGroup K] [inst_4 : TopologicalSpace K] [NonarchimedeanAddGroup K], NonarchimedeanAddGroup (G × K)