no goals
α : Type u
β : Type v
G✝ : Type w
H : Type x
inst✝⁴ : TopologicalSpace G✝
inst✝³ : Group G✝
inst✝² : TopologicalGroup G✝
inst✝¹ : TopologicalSpace α
f : α → G✝
s : Set α
x✝ : α
G : Type u_1
inst✝ : Group G
t t' : TopologicalSpace G
tg : TopologicalGroup G
tg' : TopologicalGroup G
h : 𝓝 1 = 𝓝 1
x : G
⊢ 𝓝 x = 𝓝 x
rw [← @nhds_translation_mul_inv G t _ _ x, ← @nhds_translation_mul_inv G t' _ _ x, ← h]