-- Mathlib/Topology/Algebra/OpenSubgroup.lean
theorem exist_openSubgroup_sub_clopen_nhd_of_one {G : Type*} [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] [CompactSpace G] {W : Set G} (WClopen : IsClopen W) (einW : 1 ∈ W) :
    ∃ H : OpenSubgroup G, (H : Set G) ⊆ W

Proof state:
case intro
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
⊢ ∃ H, ↑H ⊆ W

Tactic:
let S : Subgroup G := {
  carrier := ⋃ n , V ^ (n + 1)
  mul_mem' := fun ha hb ↦ by
    rcases mem_iUnion.mp ha with ⟨k, hk⟩
    rcases mem_iUnion.mp hb with ⟨l, hl⟩
    apply mem_iUnion.mpr
    use k + 1 + l
    rw [add_assoc, pow_add]
    exact Set.mul_mem_mul hk hl
  one_mem' := by
    apply mem_iUnion.mpr
    use 0
    simp [mem_of_mem_nhds hV.nhd]
  inv_mem' := fun ha ↦ by
    rcases mem_iUnion.mp ha with ⟨k, hk⟩
    apply mem_iUnion.mpr
    use k
    rw [← hV.inv]
    simpa only [inv_pow, Set.mem_inv, inv_inv] using hk }

Result:
case intro
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
⊢ ∃ H, ↑H ⊆ W

Proof state:
case succ
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen (⋃ n, V ^ (n + 1))
n : ℕ
ih : W * V ^ (n + 1) ⊆ W
⊢ W * V ^ (n + 1 + 1) ⊆ W

Tactic:
rw [pow_succ, ← mul_assoc]

Result:
case succ
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen (⋃ n, V ^ (n + 1))
n : ℕ
ih : W * V ^ (n + 1) ⊆ W
⊢ W * V ^ (n + 1) * V ⊆ W

Proof state:
case h
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
x✝ : G
ha : x✝ ∈ { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯ }.carrier
k : ℕ
hk : x✝ ∈ V ^ (k + 1)
⊢ x✝⁻¹ ∈ V ^ (k + 1)

Tactic:
rw [← hV.inv]

Result:
case h
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
x✝ : G
ha : x✝ ∈ { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯ }.carrier
k : ℕ
hk : x✝ ∈ V ^ (k + 1)
⊢ x✝⁻¹ ∈ V⁻¹ ^ (k + 1)

Proof state:
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen (⋃ n, V ^ (n + 1))
mulVpow : ∀ (n : ℕ), W * V ^ (n + 1) ⊆ W
n : ℕ
x : G
xin : x ∈ V ^ (n + 1)
⊢ x ∈ W * V ^ (n + 1)

Tactic:
rw [Set.mem_mul]

Result:
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen (⋃ n, V ^ (n + 1))
mulVpow : ∀ (n : ℕ), W * V ^ (n + 1) ⊆ W
n : ℕ
x : G
xin : x ∈ V ^ (n + 1)
⊢ ∃ x_1 ∈ W, ∃ y ∈ V ^ (n + 1), x_1 * y = x

Proof state:
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
⊢ IsOpen (⋃ n, V ^ (n + 1))

Tactic:
refine isOpen_iUnion (fun n ↦ ?_)

Result:
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
n : ℕ
⊢ IsOpen (V ^ (n + 1))

Proof state:
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
a✝ b✝ : G
ha : a✝ ∈ ⋃ n, V ^ (n + 1)
hb : b✝ ∈ ⋃ n, V ^ (n + 1)
⊢ a✝ * b✝ ∈ ⋃ n, V ^ (n + 1)

Tactic:
rcases mem_iUnion.mp ha with ⟨k, hk⟩

Result:
case intro
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
a✝ b✝ : G
ha : a✝ ∈ ⋃ n, V ^ (n + 1)
hb : b✝ ∈ ⋃ n, V ^ (n + 1)
k : ℕ
hk : a✝ ∈ V ^ (k + 1)
⊢ a✝ * b✝ ∈ ⋃ n, V ^ (n + 1)

Proof state:
case succ
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen (⋃ n, V ^ (n + 1))
n : ℕ
ih : W * V ^ (n + 1) ⊆ W
⊢ W * V ^ (n + 1) * V ⊆ W

Tactic:
exact (Set.mul_subset_mul_right ih).trans hV.mul

Result:
no goals

Proof state:
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen (⋃ n, V ^ (n + 1))
n : ℕ
⊢ W * V ^ (n + 1) ⊆ W

Tactic:
induction n with
| zero => simp [hV.mul]
| succ n ih =>
  rw [pow_succ, ← mul_assoc]
  exact (Set.mul_subset_mul_right ih).trans hV.mul

Result:
no goals

Proof state:
case h
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this✝ : IsOpen (⋃ n, V ^ (n + 1))
mulVpow : ∀ (n : ℕ), W * V ^ (n + 1) ⊆ W
this : ∀ (n : ℕ), V ^ (n + 1) ⊆ W * V ^ (n + 1)
⊢ ↑{ toSubgroup := S, isOpen' := this✝ } ⊆ W

Tactic:
apply iUnion_subset fun i _ a ↦ mulVpow i (this i a)

Result:
no goals

Proof state:
case intro.intro
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
a✝ b✝ : G
ha : a✝ ∈ ⋃ n, V ^ (n + 1)
hb : b✝ ∈ ⋃ n, V ^ (n + 1)
k : ℕ
hk : a✝ ∈ V ^ (k + 1)
l : ℕ
hl : b✝ ∈ V ^ (l + 1)
⊢ ∃ i, a✝ * b✝ ∈ V ^ (i + 1)

Tactic:
use k + 1 + l

Result:
case h
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
a✝ b✝ : G
ha : a✝ ∈ ⋃ n, V ^ (n + 1)
hb : b✝ ∈ ⋃ n, V ^ (n + 1)
k : ℕ
hk : a✝ ∈ V ^ (k + 1)
l : ℕ
hl : b✝ ∈ V ^ (l + 1)
⊢ a✝ * b✝ ∈ V ^ (k + 1 + l + 1)