-- Mathlib/Topology/Algebra/Group/Basic.lean
@[to_additive]
lemma compl_mul_closure_one_eq {t : Set G} (ht : t * (closure {1} : Set G) = t) :
    tᶜ * (closure {1} : Set G) = tᶜ

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ ↑⊥.topologicalClosure
H : (fun x1 x2 => x1 * x2) x g ∉ tᶜ
⊢ x ∈ t * ↑⊥.topologicalClosure

Tactic:
simp only [smul_eq_mul, mem_compl_iff, not_not] at H

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ ↑⊥.topologicalClosure
H : x * g ∈ t
⊢ x ∈ t * ↑⊥.topologicalClosure

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure {1} = t
⊢ tᶜ * closure {1} ⊆ tᶜ

Tactic:
rintro - ⟨x, hx, g, hg, rfl⟩

Result:
case intro.intro.intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ closure {1}
⊢ (fun x1 x2 => x1 * x2) x g ∈ tᶜ

Proof state:
case intro.intro.intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ closure {1}
⊢ (fun x1 x2 => x1 * x2) x g ∈ tᶜ

Tactic:
by_contra H

Result:
case intro.intro.intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ closure {1}
H : (fun x1 x2 => x1 * x2) x g ∉ tᶜ
⊢ False

Proof state:
case intro.intro.intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ closure {1}
H : (fun x1 x2 => x1 * x2) x g ∉ tᶜ
this : x ∈ t
⊢ False

Tactic:
exact hx this

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ closure {1}
H : (fun x1 x2 => x1 * x2) x g ∉ tᶜ
⊢ x ∈ t * closure {1}

Tactic:
rw [← Subgroup.coe_topologicalClosure_bot G] at hg ⊢

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ ↑⊥.topologicalClosure
H : (fun x1 x2 => x1 * x2) x g ∉ tᶜ
⊢ x ∈ t * ↑⊥.topologicalClosure

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ ↑⊥.topologicalClosure
H : x * g ∈ t
⊢ x ∈ t * ↑⊥.topologicalClosure

Tactic:
exact ⟨x * g, H, g⁻¹, Subgroup.inv_mem _ hg, by simp⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ closure {1}
H : (fun x1 x2 => x1 * x2) x g ∉ tᶜ
this : x ∈ t * closure {1}
⊢ False

Tactic:
rw [ht] at this

Result:
case intro.intro.intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ closure {1}
H : (fun x1 x2 => x1 * x2) x g ∉ tᶜ
this : x ∈ t
⊢ False

Proof state:
case intro.intro.intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ closure {1}
H : (fun x1 x2 => x1 * x2) x g ∉ tᶜ
⊢ False

Tactic:
have : x ∈ t * (closure {1} : Set G) := by
  rw [← Subgroup.coe_topologicalClosure_bot G] at hg ⊢
  simp only [smul_eq_mul, mem_compl_iff, not_not] at H
  exact ⟨x * g, H, g⁻¹, Subgroup.inv_mem _ hg, by simp⟩

Result:
case intro.intro.intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ closure {1}
H : (fun x1 x2 => x1 * x2) x g ∉ tᶜ
this : x ∈ t * closure {1}
⊢ False

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ ↑⊥.topologicalClosure
H : x * g ∈ t
⊢ (fun x1 x2 => x1 * x2) (x * g) g⁻¹ = x

Tactic:
simp

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure {1} = t
⊢ tᶜ * closure {1} = tᶜ

Tactic:
refine Subset.antisymm ?_ (subset_mul_closure_one tᶜ)

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure {1} = t
⊢ tᶜ * closure {1} ⊆ tᶜ