-- Mathlib/Topology/Algebra/Group/SubmonoidClosure.lean
theorem topologicalClosure_subgroupClosure_toSubmonoid (s : Set G) :
    (Subgroup.closure s).toSubmonoid.topologicalClosure =
      (Submonoid.closure s).topologicalClosure

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
x : G
hx : x ∈ s⁻¹
⊢ x⁻¹ ∈ (Subgroup.zpowers x⁻¹).topologicalClosure

Tactic:
exact subset_closure <| Subgroup.mem_zpowers _

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
x : G
hx : x ∈ s⁻¹
⊢ x ∈ closure ↑(Submonoid.powers x⁻¹)

Tactic:
rw [Submonoid.coe_powers, ← closure_range_zpow_eq_pow, ← Subgroup.coe_zpowers,
  ← Subgroup.topologicalClosure_coe, SetLike.mem_coe, ← inv_mem_iff]

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
x : G
hx : x ∈ s⁻¹
⊢ x⁻¹ ∈ (Subgroup.zpowers x⁻¹).topologicalClosure

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
⊢ s ∪ s⁻¹ ⊆ ↑(Submonoid.closure s).topologicalClosure

Tactic:
refine union_subset (Submonoid.subset_closure.trans subset_closure) fun x hx ↦ ?_

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
x : G
hx : x ∈ s⁻¹
⊢ x ∈ ↑(Submonoid.closure s).topologicalClosure

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
⊢ (Subgroup.closure s).toSubmonoid ≤ (Submonoid.closure s).topologicalClosure

Tactic:
rw [Subgroup.closure_toSubmonoid, Submonoid.closure_le]

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
⊢ s ∪ s⁻¹ ⊆ ↑(Submonoid.closure s).topologicalClosure

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
⊢ (Subgroup.closure s).topologicalClosure = (Submonoid.closure s).topologicalClosure

Tactic:
refine le_antisymm ?_ (closure_mono <| Subgroup.le_closure_toSubmonoid _)

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
⊢ (Subgroup.closure s).topologicalClosure ≤ (Submonoid.closure s).topologicalClosure

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
x : G
hx : x ∈ s⁻¹
⊢ x ∈ ↑(Submonoid.closure s).topologicalClosure

Tactic:
refine closure_mono (Submonoid.powers_le.2 (Submonoid.subset_closure <| Set.mem_inv.1 hx)) ?_

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
x : G
hx : x ∈ s⁻¹
⊢ x ∈ closure ↑(Submonoid.powers x⁻¹)

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
⊢ (Subgroup.closure s).topologicalClosure ≤ (Submonoid.closure s).topologicalClosure

Tactic:
refine Submonoid.topologicalClosure_minimal _ ?_ isClosed_closure

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
⊢ (Subgroup.closure s).toSubmonoid ≤ (Submonoid.closure s).topologicalClosure