no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
x : G
⊢ comap (fun x_1 => x_1 / x) (𝓝 1) = 𝓝 x
simpa only [div_eq_mul_inv] using nhds_translation_mul_inv x