∀ {G : Type u} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G],
  Filter.Tendsto (Function.uncurry fun x1 x2 => x1 + x2) (nhds 0 ×ˢ nhds 0) (nhds 0) →
    Filter.Tendsto (fun x => -x) (nhds 0) (nhds 0) →
      (∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) → IsTopologicalAddGroup G