-- Mathlib/Topology/Algebra/OpenSubgroup.lean
theorem isClosed [ContinuousMul G] (U : OpenSubgroup G) : IsClosed (U : Set G)

Proof state:
case refine_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : OpenSubgroup G
x : G
hx : x ∈ (↑U)ᶜ
u : G
hux : u ∈ (fun y => y * x⁻¹) ⁻¹' ↑U
hu : u ∈ ↑U
⊢ x ∈ ↑U

Tactic:
simp only [Set.mem_preimage, SetLike.mem_coe] at hux hu ⊢

Result:
case refine_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : OpenSubgroup G
x : G
hx : x ∈ (↑U)ᶜ
u : G
hux : u * x⁻¹ ∈ U
hu : u ∈ U
⊢ x ∈ U

Proof state:
case refine_2
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : OpenSubgroup G
x : G
hx : x ∈ (↑U)ᶜ
⊢ IsOpen ((fun y => y * x⁻¹) ⁻¹' ↑U)

Tactic:
exact U.isOpen.preimage (continuous_mul_right _)

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : OpenSubgroup G
⊢ IsOpen (↑U)ᶜ

Tactic:
refine isOpen_iff_forall_mem_open.2 fun x hx ↦ ⟨(fun y ↦ y * x⁻¹) ⁻¹' U, ?_, ?_, ?_⟩

Result:
case refine_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : OpenSubgroup G
x : G
hx : x ∈ (↑U)ᶜ
⊢ (fun y => y * x⁻¹) ⁻¹' ↑U ⊆ (↑U)ᶜ

case refine_2
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : OpenSubgroup G
x : G
hx : x ∈ (↑U)ᶜ
⊢ IsOpen ((fun y => y * x⁻¹) ⁻¹' ↑U)

case refine_3
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : OpenSubgroup G
x : G
hx : x ∈ (↑U)ᶜ
⊢ x ∈ (fun y => y * x⁻¹) ⁻¹' ↑U

Proof state:
case refine_3
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : OpenSubgroup G
x : G
hx : x ∈ (↑U)ᶜ
⊢ x ∈ (fun y => y * x⁻¹) ⁻¹' ↑U

Tactic:
simp [one_mem]

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : OpenSubgroup G
⊢ IsClosed ↑U

Tactic:
apply isOpen_compl_iff.1

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : OpenSubgroup G
⊢ IsOpen (↑U)ᶜ

Proof state:
case refine_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : OpenSubgroup G
x : G
hx : x ∈ (↑U)ᶜ
⊢ (fun y => y * x⁻¹) ⁻¹' ↑U ⊆ (↑U)ᶜ

Tactic:
refine fun u hux hu ↦ hx ?_

Result:
case refine_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : OpenSubgroup G
x : G
hx : x ∈ (↑U)ᶜ
u : G
hux : u ∈ (fun y => y * x⁻¹) ⁻¹' ↑U
hu : u ∈ ↑U
⊢ x ∈ ↑U

Proof state:
case h.e'_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : OpenSubgroup G
x : G
hx : x ∈ (↑U)ᶜ
u : G
hux : u * x⁻¹ ∈ U
hu : u ∈ U
⊢ x = (u * x⁻¹)⁻¹ * u

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : OpenSubgroup G
x : G
hx : x ∈ (↑U)ᶜ
u : G
hux : u * x⁻¹ ∈ U
hu : u ∈ U
⊢ x ∈ U

Tactic:
convert U.mul_mem (U.inv_mem hux) hu

Result:
case h.e'_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : OpenSubgroup G
x : G
hx : x ∈ (↑U)ᶜ
u : G
hux : u * x⁻¹ ∈ U
hu : u ∈ U
⊢ x = (u * x⁻¹)⁻¹ * u