G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
⊢ T2Space G ↔ IsClosed {1}
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
⊢ T2Space G ↔ IsClosed {1}
haveI : UniformGroup G := comm_topologicalGroup_is_uniform
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
⊢ 𝓢 G = idRel ↔ closure {1} = {1}
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
⊢ T2Space G ↔ IsClosed {1}
rw [← separated_iff_t2, separatedSpace_iff, ← closure_eq_iff_isClosed]
case mp
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
h : 𝓢 G = idRel
⊢ closure {1} = {1}

case mpr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
h : closure {1} = {1}
⊢ 𝓢 G = idRel
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
⊢ 𝓢 G = idRel ↔ closure {1} = {1}
constructor <;> intro h
case mp.h₁
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
h : 𝓢 G = idRel
⊢ closure {1} ⊆ {1}

case mp.h₂
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
h : 𝓢 G = idRel
⊢ {1} ⊆ closure {1}
case mp
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
h : 𝓢 G = idRel
⊢ closure {1} = {1}
apply Subset.antisymm
case mp.h₁
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
h : 𝓢 G = idRel
x : G
x_in : x ∈ closure {1}
⊢ x ∈ {1}
case mp.h₁
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
h : 𝓢 G = idRel
⊢ closure {1} ⊆ {1}
intro x x_in
case mp.h₁
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this✝ : UniformGroup G
h : 𝓢 G = idRel
x : G
x_in : x ∈ closure {1}
this : (x, 1) ∈ 𝓢 G ↔ x / 1 ∈ closure {1}
⊢ x ∈ {1}
case mp.h₁
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
h : 𝓢 G = idRel
x : G
x_in : x ∈ closure {1}
⊢ x ∈ {1}
have := group_separationRel x 1
case mp.h₁
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this✝ : UniformGroup G
h : 𝓢 G = idRel
x : G
x_in : x ∈ closure {1}
this : (x, 1) ∈ 𝓢 G ↔ x ∈ closure {1}
⊢ x ∈ {1}
case mp.h₁
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this✝ : UniformGroup G
h : 𝓢 G = idRel
x : G
x_in : x ∈ closure {1}
this : (x, 1) ∈ 𝓢 G ↔ x / 1 ∈ closure {1}
⊢ x ∈ {1}
rw [div_one] at this
case mp.h₁
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this✝ : UniformGroup G
h : 𝓢 G = idRel
x : G
x_in : (x, 1) ∈ idRel
this : (x, 1) ∈ 𝓢 G ↔ x ∈ closure {1}
⊢ x ∈ {1}
case mp.h₁
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this✝ : UniformGroup G
h : 𝓢 G = idRel
x : G
x_in : x ∈ closure {1}
this : (x, 1) ∈ 𝓢 G ↔ x ∈ closure {1}
⊢ x ∈ {1}
rw [← this, h] at x_in
no goals
case mp.h₁
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this✝ : UniformGroup G
h : 𝓢 G = idRel
x : G
x_in : (x, 1) ∈ idRel
this : (x, 1) ∈ 𝓢 G ↔ x ∈ closure {1}
⊢ x ∈ {1}
rwa [mem_singleton_iff]
no goals
case mp.h₂
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
h : 𝓢 G = idRel
⊢ {1} ⊆ closure {1}
exact subset_closure
case mpr.h
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
h : closure {1} = {1}
p : G × G
⊢ p ∈ 𝓢 G ↔ p ∈ idRel
case mpr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
h : closure {1} = {1}
⊢ 𝓢 G = idRel
ext p
case mpr.h.mk
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
h : closure {1} = {1}
x y : G
⊢ (x, y) ∈ 𝓢 G ↔ (x, y) ∈ idRel
case mpr.h
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
h : closure {1} = {1}
p : G × G
⊢ p ∈ 𝓢 G ↔ p ∈ idRel
cases' p with x y
case mpr.h.mk
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
h : closure {1} = {1}
x y : G
⊢ x = y ↔ (x, y) ∈ idRel
case mpr.h.mk
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
h : closure {1} = {1}
x y : G
⊢ (x, y) ∈ 𝓢 G ↔ (x, y) ∈ idRel
rw [group_separationRel x, h, mem_singleton_iff, div_eq_one]
no goals
case mpr.h.mk
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
this : UniformGroup G
h : closure {1} = {1}
x y : G
⊢ x = y ↔ (x, y) ∈ idRel
rfl