case a
G✝ : Type ?u.426706
inst✝⁴ : CommGroup G✝
inst✝³ : TopologicalSpace G✝
inst✝² : TopologicalGroup G✝
G : Type u_1
u : UniformSpace G
inst✝¹ : Group G
inst✝ : UniformGroup G
⊢ 𝓤 G = 𝓤 G
G✝ : Type ?u.426706
inst✝⁴ : CommGroup G✝
inst✝³ : TopologicalSpace G✝
inst✝² : TopologicalGroup G✝
G : Type u_1
u : UniformSpace G
inst✝¹ : Group G
inst✝ : UniformGroup G
⊢ TopologicalGroup.toUniformSpace G = u
ext : 1
no goals
case a
G✝ : Type ?u.426706
inst✝⁴ : CommGroup G✝
inst✝³ : TopologicalSpace G✝
inst✝² : TopologicalGroup G✝
G : Type u_1
u : UniformSpace G
inst✝¹ : Group G
inst✝ : UniformGroup G
⊢ 𝓤 G = 𝓤 G
rw [uniformity_eq_comap_nhds_one' G, uniformity_eq_comap_nhds_one G]