∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] (S : AddSubgroup G)
  (motive : (∃ U ∈ nhds 0, -U = U ∧ ∀ g ∈ S, ((fun x => g + x) '' U ∩ U).Nonempty → g = 0) → Prop)
  (x : ∃ U ∈ nhds 0, -U = U ∧ ∀ g ∈ S, ((fun x => g + x) '' U ∩ U).Nonempty → g = 0),
  (∀ (U : Set G) (hU : U ∈ nhds 0) (hUinv : -U = U) (h : ∀ g ∈ S, ((fun x => g + x) '' U ∩ U).Nonempty → g = 0),
      motive ⋯) →
    motive x