∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] {W : Set G} (x : Set G)
  (motive : (∃ T ∈ nhds 0, x + T ⊆ W) → Prop) (x_1 : ∃ T ∈ nhds 0, x + T ⊆ W),
  (∀ (T : Set G) (hT : T ∈ nhds 0) (mem : x + T ⊆ W), motive ⋯) → motive x_1