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