no goals
α : Type ?u.165655
β : Type ?u.165658
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
G : Type u_1
inst✝ : Group G
u v : UniformSpace G
hu : UniformGroup G
hv : UniformGroup G
h : 𝓝 1 = 𝓝 1
⊢ 𝓤 G = 𝓤 G
rw [@uniformity_eq_comap_nhds_one _ u _ hu, @uniformity_eq_comap_nhds_one _ v _ hv, h]