G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
⊢ ∀ (a : G), a ∈ {1}ᶜ → {1}ᶜ ∈ 𝓝 a
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
⊢ T2Space G
rw [TopologicalGroup.t2Space_iff_one_closed, ← isOpen_compl_iff, isOpen_iff_mem_nhds]
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
⊢ {1}ᶜ ∈ 𝓝 x
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
⊢ ∀ (a : G), a ∈ {1}ᶜ → {1}ᶜ ∈ 𝓝 a
intro x x_not
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
this : x ≠ 1
⊢ {1}ᶜ ∈ 𝓝 x
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
⊢ {1}ᶜ ∈ 𝓝 x
have : x ≠ 1 := mem_compl_singleton_iff.mp x_not
case intro.intro
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
this : x ≠ 1
U : Set G
U_in : U ∈ 𝓝 1
xU : ¬x ∈ U
⊢ {1}ᶜ ∈ 𝓝 x
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
this : x ≠ 1
⊢ {1}ᶜ ∈ 𝓝 x
rcases H x this with ⟨U, U_in, xU⟩
case intro.intro
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
this : x ≠ 1
U : Set G
U_in : U ∈ comap Inv.inv (𝓝 1)
xU : ¬x ∈ U
⊢ {1}ᶜ ∈ 𝓝 x
case intro.intro
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
this : x ≠ 1
U : Set G
U_in : U ∈ 𝓝 1
xU : ¬x ∈ U
⊢ {1}ᶜ ∈ 𝓝 x
rw [← nhds_one_symm G] at U_in
case intro.intro.intro.intro
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
this : x ≠ 1
U : Set G
xU : ¬x ∈ U
W : Set G
W_in : W ∈ 𝓝 1
UW : Inv.inv ⁻¹' W ⊆ U
⊢ {1}ᶜ ∈ 𝓝 x
case intro.intro
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
this : x ≠ 1
U : Set G
U_in : U ∈ comap Inv.inv (𝓝 1)
xU : ¬x ∈ U
⊢ {1}ᶜ ∈ 𝓝 x
rcases U_in with ⟨W, W_in, UW⟩
case intro.intro.intro.intro
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
this : x ≠ 1
U : Set G
xU : ¬x ∈ U
W : Set G
W_in : W ∈ 𝓝 1
UW : Inv.inv ⁻¹' W ⊆ U
⊢ {1}ᶜ ∈ comap (fun y => y * x⁻¹) (𝓝 1)
case intro.intro.intro.intro
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
this : x ≠ 1
U : Set G
xU : ¬x ∈ U
W : Set G
W_in : W ∈ 𝓝 1
UW : Inv.inv ⁻¹' W ⊆ U
⊢ {1}ᶜ ∈ 𝓝 x
rw [← nhds_translation_mul_inv]
case intro.intro.intro.intro
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
this : x ≠ 1
U : Set G
xU : ¬x ∈ U
W : Set G
W_in : W ∈ 𝓝 1
UW : Inv.inv ⁻¹' W ⊆ U
⊢ (fun y => y * x⁻¹) ⁻¹' W ⊆ {1}ᶜ
case intro.intro.intro.intro
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
this : x ≠ 1
U : Set G
xU : ¬x ∈ U
W : Set G
W_in : W ∈ 𝓝 1
UW : Inv.inv ⁻¹' W ⊆ U
⊢ {1}ᶜ ∈ comap (fun y => y * x⁻¹) (𝓝 1)
use W, W_in
case intro.intro.intro.intro
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
this : x ≠ 1
U : Set G
xU : ¬x ∈ U
W : Set G
W_in : W ∈ 𝓝 1
UW : Inv.inv ⁻¹' W ⊆ U
⊢ {1} ⊆ ((fun y => y * x⁻¹) ⁻¹' W)ᶜ
case intro.intro.intro.intro
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
this : x ≠ 1
U : Set G
xU : ¬x ∈ U
W : Set G
W_in : W ∈ 𝓝 1
UW : Inv.inv ⁻¹' W ⊆ U
⊢ (fun y => y * x⁻¹) ⁻¹' W ⊆ {1}ᶜ
rw [subset_compl_comm]
case intro.intro.intro.intro
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
this : x ≠ 1
U : Set G
xU : ¬x ∈ U
W : Set G
W_in : W ∈ 𝓝 1
UW : Inv.inv ⁻¹' W ⊆ U
⊢ ¬x⁻¹ ∈ W
case intro.intro.intro.intro
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
this : x ≠ 1
U : Set G
xU : ¬x ∈ U
W : Set G
W_in : W ∈ 𝓝 1
UW : Inv.inv ⁻¹' W ⊆ U
⊢ {1} ⊆ ((fun y => y * x⁻¹) ⁻¹' W)ᶜ
suffices x⁻¹ ∉ W by simpa
no goals
case intro.intro.intro.intro
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
this : x ≠ 1
U : Set G
xU : ¬x ∈ U
W : Set G
W_in : W ∈ 𝓝 1
UW : Inv.inv ⁻¹' W ⊆ U
⊢ ¬x⁻¹ ∈ W
exact fun h => xU (UW h)
no goals
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U, U ∈ 𝓝 1 ∧ ¬x ∈ U
x : G
x_not : x ∈ {1}ᶜ
this✝ : x ≠ 1
U : Set G
xU : ¬x ∈ U
W : Set G
W_in : W ∈ 𝓝 1
UW : Inv.inv ⁻¹' W ⊆ U
this : ¬x⁻¹ ∈ W
⊢ {1} ⊆ ((fun y => y * x⁻¹) ⁻¹' W)ᶜ
simpa