-- Mathlib/Topology/Algebra/OpenSubgroup.lean
@[to_additive]
lemma exist_mul_closure_nhd {W : Set G} (WClopen : IsClopen W) : ∃ T ∈ 𝓝 (1 : G), W * T ⊆ 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
x : G
memW : x ∈ W
⊢ ∃ t ∈ 𝓝[W] x, ∃ T ∈ 𝓝 1, t * T ⊆ W

Tactic:
have : (x, 1) ∈ (fun p ↦ p.1 * p.2) ⁻¹' W := by simp [memW]

Result:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
x : G
memW : x ∈ W
this : (x, 1) ∈ (fun p => p.1 * p.2) ⁻¹' W
⊢ ∃ t ∈ 𝓝[W] x, ∃ T ∈ 𝓝 1, t * T ⊆ 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
⊢ ∀ x ∈ W, ∃ t ∈ 𝓝[W] x, ∃ T ∈ 𝓝 1, t * T ⊆ W

Tactic:
intro x memW

Result:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
x : G
memW : x ∈ W
⊢ ∃ t ∈ 𝓝[W] x, ∃ T ∈ 𝓝 1, t * T ⊆ W

Proof state:
case intro.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
x : G
memW : x ∈ W
this : (x, 1) ∈ (fun p => p.1 * p.2) ⁻¹' W
U V : Set G
Uopen : IsOpen U
Vopen : IsOpen V
xmemU : x ∈ U
onememV : 1 ∈ V
prodsub : U ×ˢ V ⊆ (fun p => p.1 * p.2) ⁻¹' W
h6 : U * V ⊆ W
⊢ ∃ t ∈ 𝓝[W] x, ∃ T ∈ 𝓝 1, t * T ⊆ W

Tactic:
exact ⟨U ∩ W, ⟨U, Uopen.mem_nhds xmemU, W, fun _ a ↦ a, rfl⟩,
  V, IsOpen.mem_nhds Vopen onememV, fun _ a ↦ h6 ((mul_subset_mul_right inter_subset_left) a)⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
U V : Set G
x✝¹ : (fun S => ∃ T ∈ 𝓝 1, S * T ⊆ W) U
x✝ : (fun S => ∃ T ∈ 𝓝 1, S * T ⊆ W) V
T₁ : Set G
hT₁ : T₁ ∈ 𝓝 1
mem1 : U * T₁ ⊆ W
T₂ : Set G
hT₂ : T₂ ∈ 𝓝 1
mem2 : V * T₂ ⊆ W
⊢ (U ∪ V) * (T₁ ∩ T₂) ⊆ W

Tactic:
rw [union_mul]

Result:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
U V : Set G
x✝¹ : (fun S => ∃ T ∈ 𝓝 1, S * T ⊆ W) U
x✝ : (fun S => ∃ T ∈ 𝓝 1, S * T ⊆ W) V
T₁ : Set G
hT₁ : T₁ ∈ 𝓝 1
mem1 : U * T₁ ⊆ W
T₂ : Set G
hT₂ : T₂ ∈ 𝓝 1
mem2 : V * T₂ ⊆ W
⊢ U * (T₁ ∩ T₂) ∪ V * (T₁ ∩ T₂) ⊆ 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
x : G
memW : x ∈ W
⊢ (x, 1) ∈ (fun p => p.1 * p.2) ⁻¹' W

Tactic:
simp [memW]

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
x : G
memW : x ∈ W
this : (x, 1) ∈ (fun p => p.1 * p.2) ⁻¹' W
⊢ ∃ t ∈ 𝓝[W] x, ∃ T ∈ 𝓝 1, t * T ⊆ W

Tactic:
rcases isOpen_prod_iff.mp (continuous_mul.isOpen_preimage W <| WClopen.2) x 1 this with
  ⟨U, V, Uopen, Vopen, xmemU, onememV, prodsub⟩

Result:
case intro.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
x : G
memW : x ∈ W
this : (x, 1) ∈ (fun p => p.1 * p.2) ⁻¹' W
U V : Set G
Uopen : IsOpen U
Vopen : IsOpen V
xmemU : x ∈ U
onememV : 1 ∈ V
prodsub : U ×ˢ V ⊆ (fun p => p.1 * p.2) ⁻¹' W
⊢ ∃ t ∈ 𝓝[W] x, ∃ T ∈ 𝓝 1, t * T ⊆ W

Proof state:
case intro.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
x : G
memW : x ∈ W
this : (x, 1) ∈ (fun p => p.1 * p.2) ⁻¹' W
U V : Set G
Uopen : IsOpen U
Vopen : IsOpen V
xmemU : x ∈ U
onememV : 1 ∈ V
prodsub : U ×ˢ V ⊆ (fun p => p.1 * p.2) ⁻¹' W
⊢ ∃ t ∈ 𝓝[W] x, ∃ T ∈ 𝓝 1, t * T ⊆ W

Tactic:
have h6 : U * V ⊆ W := mul_subset_iff.mpr (fun _ hx _ hy ↦ prodsub (mk_mem_prod hx hy))

Result:
case intro.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
x : G
memW : x ∈ W
this : (x, 1) ∈ (fun p => p.1 * p.2) ⁻¹' W
U V : Set G
Uopen : IsOpen U
Vopen : IsOpen V
xmemU : x ∈ U
onememV : 1 ∈ V
prodsub : U ×ˢ V ⊆ (fun p => p.1 * p.2) ⁻¹' W
h6 : U * V ⊆ W
⊢ ∃ t ∈ 𝓝[W] x, ∃ T ∈ 𝓝 1, t * T ⊆ 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
⊢ univ ∈ 𝓝 1 ∧ ∅ * univ ⊆ W

Tactic:
simp only [univ_mem, empty_mul, empty_subset, and_self]

Result:
no goals

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 ∈ 𝓝 1, W * T ⊆ W

Tactic:
apply WClopen.isClosed.isCompact.induction_on (p := fun S ↦ ∃ T ∈ 𝓝 (1 : G), S * T ⊆ W)
  ⟨Set.univ ,by simp only [univ_mem, empty_mul, empty_subset, and_self]⟩
  (fun _ _ huv ⟨T, hT, mem⟩ ↦ ⟨T, hT, (mul_subset_mul_right huv).trans mem⟩)
  fun U V ⟨T₁, hT₁, mem1⟩ ⟨T₂, hT₂, mem2⟩ ↦ ⟨T₁ ∩ T₂, inter_mem hT₁ hT₂, by
    rw [union_mul]
    exact union_subset (mul_subset_mul_left inter_subset_left |>.trans mem1)
      (mul_subset_mul_left inter_subset_right |>.trans mem2) ⟩

Result:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
⊢ ∀ x ∈ W, ∃ t ∈ 𝓝[W] x, ∃ T ∈ 𝓝 1, t * T ⊆ 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
U V : Set G
x✝¹ : (fun S => ∃ T ∈ 𝓝 1, S * T ⊆ W) U
x✝ : (fun S => ∃ T ∈ 𝓝 1, S * T ⊆ W) V
T₁ : Set G
hT₁ : T₁ ∈ 𝓝 1
mem1 : U * T₁ ⊆ W
T₂ : Set G
hT₂ : T₂ ∈ 𝓝 1
mem2 : V * T₂ ⊆ W
⊢ U * (T₁ ∩ T₂) ∪ V * (T₁ ∩ T₂) ⊆ W

Tactic:
exact union_subset (mul_subset_mul_left inter_subset_left |>.trans mem1)
  (mul_subset_mul_left inter_subset_right |>.trans mem2)

Result:
no goals