-- Mathlib/Topology/Algebra/OpenSubgroup.lean
@[to_additive]
lemma exists_mulInvClosureNhd {W : Set G} (WClopen : IsClopen W) :
    ∃ T, mulInvClosureNhd T W

Proof state:
case h
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen U
onememU : 1 ∈ U
⊢ mulInvClosureNhd (U ∩ U⁻¹) W

Tactic:
constructor

Result:
case h.nhd
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen U
onememU : 1 ∈ U
⊢ U ∩ U⁻¹ ∈ 𝓝 1

case h.inv
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen U
onememU : 1 ∈ U
⊢ (U ∩ U⁻¹)⁻¹ = U ∩ U⁻¹

case h.isOpen
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen U
onememU : 1 ∈ U
⊢ IsOpen (U ∩ U⁻¹)

case h.mul
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen U
onememU : 1 ∈ U
⊢ W * (U ∩ U⁻¹) ⊆ W

Proof state:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
⊢ ∃ T, mulInvClosureNhd T W

Tactic:
rcases exist_mul_closure_nhd WClopen with ⟨S, Smemnhds, mulclose⟩

Result:
case intro.intro
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
⊢ ∃ T, mulInvClosureNhd T W

Proof state:
case h.mul
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen U
onememU : 1 ∈ U
⊢ W * (U ∩ U⁻¹) ⊆ W

Tactic:
exact fun a ha ↦ mulclose (mul_subset_mul_left UsubS (mul_subset_mul_left inter_subset_left ha))

Result:
no goals

Proof state:
case h.nhd
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen U
onememU : 1 ∈ U
⊢ U ∩ U⁻¹ ∈ 𝓝 1

Tactic:
simp [Uopen.mem_nhds onememU, inv_mem_nhds_one]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen U
onememU : 1 ∈ U
⊢ ∃ T, mulInvClosureNhd T W

Tactic:
use U ∩ U⁻¹

Result:
case h
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen U
onememU : 1 ∈ U
⊢ mulInvClosureNhd (U ∩ U⁻¹) W

Proof state:
case h.isOpen
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen U
onememU : 1 ∈ U
⊢ IsOpen (U ∩ U⁻¹)

Tactic:
exact Uopen.inter Uopen.inv

Result:
no goals

Proof state:
case h.inv
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen U
onememU : 1 ∈ U
⊢ (U ∩ U⁻¹)⁻¹ = U ∩ U⁻¹

Tactic:
simp [inter_comm]

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
⊢ ∃ T, mulInvClosureNhd T W

Tactic:
rcases mem_nhds_iff.mp Smemnhds with ⟨U, UsubS, Uopen, onememU⟩

Result:
case intro.intro.intro.intro.intro
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen U
onememU : 1 ∈ U
⊢ ∃ T, mulInvClosureNhd T W