awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s : Set G
hs : IsOpen[inst] s
t : Set G
refine : ∀ (a : G) (ha : a ∈ s) (b : G) (hb : b ∈ closure[inst] t), a * b ∈ s * t
⊢ s * closure[inst] t = s * t

Tactic:
refine (mul_subset_iff.2 fun a ha b hb => ?_).antisymm (mul_subset_mul_left subset_closure)

Premises used: Iff.mpr, subset_closure, Set.mul_subset_iff, HasSubset.Subset.antisymm, Set.mul_subset_mul_left
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s : Set G
hs : IsOpen[inst] s
t : Set G
a : G
ha : a ∈ s
b : G
hb : b ∈ closure[inst] t
⊢ ∀ (o : Set G), IsOpen[inst] o → b ∈ o → (o ∩ t).Nonempty

Tactic:
rw [mem_closure_iff] at hb

Premises used: mem_closure_iff
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s : Set G
hs : IsOpen[inst] s
t : Set G
a : G
ha : a ∈ s
b : G
hb : ∀ (o : Set G), IsOpen[inst] o → b ∈ o → (o ∩ t).Nonempty
⊢ b ∈ s⁻¹ * {a * b}

Tactic:
have hbU : b ∈ s⁻¹ * {a * b} := ⟨a⁻¹, Set.inv_mem_inv.2 ha, a * b, rfl, inv_mul_cancel_left _ _⟩
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s : Set G
hs : IsOpen[inst] s
t : Set G
a : G
ha : a ∈ s
b : G
hb : ∀ (o : Set G), IsOpen[inst] o → b ∈ o → (o ∩ t).Nonempty
hbU : b ∈ s⁻¹ * {a * b}
obtain : ∀ (c : G) (hc : c ∈ s⁻¹) (hcs : (fun (x1 x2 : G) ↦ x1 * x2) c (a * b) ∈ t), a * b ∈ s * t
⊢ a * b ∈ s * t

Tactic:
obtain ⟨_, ⟨c, hc, d, rfl : d = _, rfl⟩, hcs⟩ := hb _ hs.inv.mul_right hbU

Premises used: IsOpen.inv, IsOpen.mul_right, rfl
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s : Set G
hs : IsOpen[inst] s
t : Set G
a : G
ha : a ∈ s
b : G
hb : ∀ (o : Set G), IsOpen[inst] o → b ∈ o → (o ∩ t).Nonempty
hbU : b ∈ s⁻¹ * {a * b}
c : G
hc : c ∈ s⁻¹
hcs : (fun (x1 x2 : G) ↦ x1 * x2) c (a * b) ∈ t
⊢ a * b ∈ s * t

Tactic:
⟨c⁻¹, hc, _, hcs, inv_mul_cancel_left _ _⟩

Premises used: inv_mul_cancel_left, Set.Mem, setOf, Inv.inv, Set.image2, And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s : Set G
hs : IsOpen[inst] s
t : Set G
a : G
ha : a ∈ s
b : G
hb : ∀ (o : Set G), IsOpen[inst] o → b ∈ o → (o ∩ t).Nonempty
hbU : b ∈ s⁻¹ * {a * b}
c : G
hc : c ∈ s⁻¹
hcs : (fun (x1 x2 : G) ↦ x1 * x2) c (a * b) ∈ t
⊢ a * b ∈ s * t

Tactic:
exact ⟨c⁻¹, hc, _, hcs, inv_mul_cancel_left _ _⟩
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : IsOpen[inst] t
s : Set G
rw : (closure[inst] s * t)⁻¹⁻¹ = s * t
rw₁ : (t⁻¹ * (closure[inst] s)⁻¹)⁻¹ = s * t
rw₂ : (t⁻¹ * closure[inst] s⁻¹)⁻¹ = s * t
rw₃ : (t⁻¹ * s⁻¹)⁻¹ = s * t
rw₄ : s⁻¹⁻¹ * t⁻¹⁻¹ = s * t
rw₅ : s * t⁻¹⁻¹ = s * t
rw₆ rw₇ : s * t = s * t
⊢ closure[inst] s * t = s * t

Tactic:
rw [← inv_inv (closure s * t), mul_inv_rev, inv_closure, ht.inv.mul_closure, mul_inv_rev, inv_inv,
    inv_inv]

Premises used: HMul.hMul, closure, inv_inv, IsOpen.inv, mul_inv_rev, IsOpen.mul_closure, inv_closure
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s : Set G
hs : IsOpen[inst] s
t : Set G
simp_rw : s * (closure[inst] t)⁻¹ = s * t⁻¹
simp_rw₁ : s * closure[inst] t⁻¹ = s * t⁻¹
⊢ s / closure[inst] t = s / t

Tactic:
simp_rw [div_eq_mul_inv, inv_closure, hs.mul_closure]

Premises used: div_eq_mul_inv, IsOpen.mul_closure, inv_closure
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : IsOpen[inst] t
s : Set G
simp_rw : closure[inst] s * t⁻¹ = s * t⁻¹
⊢ closure[inst] s / t = s / t

Tactic:
simp_rw [div_eq_mul_inv, ht.inv.closure_mul]

Premises used: div_eq_mul_inv, IsOpen.inv, IsOpen.closure_mul
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s t : Set G
ht : IsClosed[inst] t
hs : IsCompact s
⊢ IsClosed[inst] (s * t)

Tactic:
ht.smul_left_of_isCompact hs

Premises used: IsClosed.smul_left_of_isCompact
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s t : Set G
ht : IsClosed[inst] t
hs : IsCompact s
rw : IsClosed[inst] (op '' s • t)
⊢ IsClosed[inst] (t * s)

Tactic:
rw [← image_op_smul]

Premises used: Set.image_op_smul
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s t : Set G
ht : IsClosed[inst] t
hs : IsCompact s
⊢ IsClosed[inst] (op '' s • t)

Tactic:
IsClosed.smul_left_of_isCompact ht (hs.image continuous_op)

Premises used: IsClosed.smul_left_of_isCompact, IsCompact.image, MulOpposite.continuous_op
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
s t : Set G
ht : IsClosed[inst] t
hs : IsCompact s
⊢ IsClosed[inst] (op '' s • t)

Tactic:
exact IsClosed.smul_left_of_isCompact ht (hs.image continuous_op)

Premises used: IsClosed.smul_left_of_isCompact, IsCompact.image, MulOpposite.continuous_op
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type u_1
inst : MulOneClass G
inst_1 : TopologicalSpace G
s : Set G
⊢ s ⊆ s * {1}

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type u_1
inst : MulOneClass G
inst_1 : TopologicalSpace G
s : Set G
⊢ s ⊆ s * {1}

Tactic:
have : s ⊆ s * ({1} : Set G) := by simp
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type u_1
inst : MulOneClass G
inst_1 : TopologicalSpace G
s : Set G
this : s ⊆ s * {1}
⊢ s ⊆ s * closure[inst_1] {1}

Tactic:
this.trans (smul_subset_smul_left subset_closure)

Premises used: subset_closure, Set.smul_subset_smul_left, HasSubset.Subset.trans
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type u_1
inst : MulOneClass G
inst_1 : TopologicalSpace G
s : Set G
this : s ⊆ s * {1}
⊢ s ⊆ s * closure[inst_1] {1}

Tactic:
exact this.trans (smul_subset_smul_left subset_closure)

Premises used: subset_closure, Set.smul_subset_smul_left, HasSubset.Subset.trans
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
apply : K * closure[inst] {1} ⊆ closure[inst] K
apply₁ : closure[inst] K ⊆ K * closure[inst] {1}
⊢ K * closure[inst] {1} = closure[inst] K

Tactic:
apply Subset.antisymm ?_ ?_

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ K * closure[inst] {1} ⊆ closure[inst] K * closure[inst] {1}

Tactic:
smul_subset_smul_right subset_closure

Premises used: subset_closure, Set.smul_subset_smul_right
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ closure[inst] K * closure[inst] {1} ⊆ closure[inst] (K * {1})

Tactic:
smul_set_closure_subset _ _

Premises used: smul_set_closure_subset
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ closure[inst] (K * {1}) = closure[inst] K

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
K₁ : closure[inst] (K * {1}) = closure[inst] K
⊢ K * closure[inst] {1} ⊆ closure[inst] K

Tactic:
calc
    K * (closure {1} : Set G) ⊆ closure K * (closure {1} : Set G) :=
      smul_subset_smul_right subset_closure
    _ ⊆ closure (K * ({1} : Set G)) := smul_set_closure_subset _ _
    _ = closure K := by simp

Premises used: HMul.hMul, subset_closure, closure, smul_set_closure_subset, Set.smul_subset_smul_right, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ IsClosed[inst] (K * closure[inst] {1})

Tactic:
have : IsClosed (K * (closure {1} : Set G)) :=
      IsClosed.smul_left_of_isCompact isClosed_closure hK
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
this : IsClosed[inst] (K * closure[inst] {1})
rw : K ⊆ K * closure[inst] {1}
⊢ closure[inst] K ⊆ K * closure[inst] {1}

Tactic:
rw [IsClosed.closure_subset_iff this]

Premises used: IsClosed.closure_subset_iff
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
this : IsClosed[inst] (K * closure[inst] {1})
⊢ K ⊆ K * closure[inst] {1}

Tactic:
subset_mul_closure_one K

Premises used: subset_mul_closure_one
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
this : IsClosed[inst] (K * closure[inst] {1})
⊢ K ⊆ K * closure[inst] {1}

Tactic:
exact subset_mul_closure_one K

Premises used: subset_mul_closure_one
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
F : Set G
hF : IsClosed[inst] F
⊢ F * closure[inst] {1} = F

Tactic:
Subset.antisymm ?_ (subset_mul_closure_one F)

Premises used: Set.Subset.antisymm, subset_mul_closure_one
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
F : Set G
hF : IsClosed[inst] F
refine : F * closure[inst] {1} ⊆ F
⊢ F * closure[inst] {1} = F

Tactic:
refine Subset.antisymm ?_ (subset_mul_closure_one F)

Premises used: Set.Subset.antisymm, subset_mul_closure_one
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
F : Set G
hF : IsClosed[inst] F
rw rw₁ : F * closure[inst] {1} = F * closure[inst] {1}
⊢ F * closure[inst] {1} = closure[inst] F * closure[inst] {1}

Tactic:
rw [hF.closure_eq]

Premises used: IsClosed.closure_eq
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
F : Set G
hF : IsClosed[inst] F
⊢ closure[inst] F * closure[inst] {1} ⊆ closure[inst] (F * {1})

Tactic:
smul_set_closure_subset _ _

Premises used: smul_set_closure_subset
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
F : Set G
hF : IsClosed[inst] F
⊢ closure[inst] (F * {1}) = F

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
F : Set G
hF : IsClosed[inst] F
F₁ : F * closure[inst] {1} = closure[inst] F * closure[inst] {1}
F₂ : closure[inst] (F * {1}) = F
⊢ F * closure[inst] {1} ⊆ F

Tactic:
calc
  F * (closure {1} : Set G) = closure F * closure ({1} : Set G) := by rw [hF.closure_eq]
  _ ⊆ closure (F * ({1} : Set G)) := smul_set_closure_subset _ _
  _ = F := by simp

Premises used: HMul.hMul, closure, smul_set_closure_subset, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : t * closure[inst] {1} = t
⊢ tᶜ * closure[inst] {1} = tᶜ

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

Premises used: Set.Subset.antisymm, Compl.compl, subset_mul_closure_one
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : t * closure[inst] {1} = t
refine : tᶜ * closure[inst] {1} ⊆ tᶜ
⊢ tᶜ * closure[inst] {1} = tᶜ

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

Premises used: Set.Subset.antisymm, Compl.compl, subset_mul_closure_one
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : t * closure[inst] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : Membership.mem (γ := Set G) (closure[inst] {1}) g
by_contra : ∀ (H : (fun (x1 x2 : G) ↦ x1 * x2) x g ∉ tᶜ), False
⊢ (fun (x1 x2 : G) ↦ x1 * x2) x g ∈ tᶜ

Tactic:
by_contra H
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : t * closure[inst] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : Membership.mem (γ := Set G) (closure[inst] {1}) g
H : (fun (x1 x2 : G) ↦ x1 * x2) x g ∉ tᶜ
rw :
  ∀ (hg : g ∈ (↑(Subgroup.topologicalClosure ⊥) : Set G)) (H : (fun (x1 x2 : G) ↦ x1 * x2) x g ∉ tᶜ),
    x ∈ t * (↑(Subgroup.topologicalClosure ⊥) : Set G)
⊢ x ∈ t * closure[inst] {1}

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

Premises used: Subgroup.coe_topologicalClosure_bot
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : t * closure[inst] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ (↑(Subgroup.topologicalClosure ⊥) : Set G)
H : (fun (x1 x2 : G) ↦ x1 * x2) x g ∉ tᶜ
⊢ x * g ∈ t

Tactic:
simp only [mem_compl_iff, not_not] at H

Premises used: Classical.not_not, Set.mem_compl_iff
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : t * closure[inst] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ (↑(Subgroup.topologicalClosure ⊥) : Set G)
H : x * g ∈ t
⊢ (fun (x1 x2 : G) ↦ x1 * x2) (x * g) g⁻¹ = x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : t * closure[inst] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ (↑(Subgroup.topologicalClosure ⊥) : Set G)
H : x * g ∈ t
⊢ x ∈ t * (↑(Subgroup.topologicalClosure ⊥) : Set G)

Tactic:
exact ⟨x * g, H, g⁻¹, Subgroup.inv_mem _ hg, by simp⟩
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : t * closure[inst] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : Membership.mem (γ := Set G) (closure[inst] {1}) g
H : (fun (x1 x2 : G) ↦ x1 * x2) x g ∉ tᶜ
⊢ x ∈ t * closure[inst] {1}

Tactic:
have : x ∈ t * (closure {1} : Set G) := by
    rw [← Subgroup.coe_topologicalClosure_bot G] at hg ⊢
    simp only [mem_compl_iff, not_not] at H
    exact ⟨x * g, H, g⁻¹, Subgroup.inv_mem _ hg, by simp⟩
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : t * closure[inst] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : Membership.mem (γ := Set G) (closure[inst] {1}) g
H : (fun (x1 x2 : G) ↦ x1 * x2) x g ∉ tᶜ
this : x ∈ t * closure[inst] {1}
⊢ x ∈ t

Tactic:
rw [ht] at this
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : t * closure[inst] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : Membership.mem (γ := Set G) (closure[inst] {1}) g
H : (fun (x1 x2 : G) ↦ x1 * x2) x g ∉ tᶜ
this : x ∈ t
⊢ False

Tactic:
hx this
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : t * closure[inst] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : Membership.mem (γ := Set G) (closure[inst] {1}) g
H : (fun (x1 x2 : G) ↦ x1 * x2) x g ∉ tᶜ
this : x ∈ t
⊢ False

Tactic:
exact hx this
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
h : tᶜ * closure[inst] {1} = tᶜ
⊢ t * closure[inst] {1} = t

Tactic:
simpa using compl_mul_closure_one_eq h

Premises used: compl_mul_closure_one_eq
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
U : Set G
hU : IsOpen[inst] U
⊢ U * closure[inst] {1} = U

Tactic:
compl_mul_closure_one_eq_iff.1 (hU.isClosed_compl.mul_closure_one_eq)

Premises used: IsClosed.mul_closure_one_eq, IsOpen.isClosed_compl, Iff.mp, compl_mul_closure_one_eq_iff
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : G
hx : x ∈ closure[inst] U
⊢ ∀ t ∈ 𝓝 x, (t ∩ U).Nonempty

Tactic:
rw [mem_closure_iff_nhds] at hx

Premises used: mem_closure_iff_nhds
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : G
hx : ∀ t ∈ 𝓝 x, (t ∩ U).Nonempty
⊢ ContinuousAt (Y := G) (fun (y : G) ↦ x / y) x

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : G
hx : ∀ t ∈ 𝓝 x, (t ∩ U).Nonempty
⊢ U ∈ 𝓝 (x / x)

Tactic:
simpa
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : G
hx : ∀ t ∈ 𝓝 x, (t ∩ U).Nonempty
⊢ (fun (y : G) ↦ x / y) ⁻¹' U ∈ 𝓝 x

Tactic:
have hkey : (fun y => x / y) ⁻¹' U ∈ 𝓝 x :=
    ContinuousAt.preimage_mem_nhds (by fun_prop) (by simpa)
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : G
hx : ∀ t ∈ 𝓝 x, (t ∩ U).Nonempty
hkey : (fun (y : G) ↦ x / y) ⁻¹' U ∈ 𝓝 x
obtain : ∀ (a : G) (ha_mem : Membership.mem (γ := Set G) ((fun (y : G) ↦ x / y) ⁻¹' U) a) (ha_s : a ∈ U), x ∈ U * U
⊢ x ∈ U * U

Tactic:
obtain ⟨a, ha_mem, ha_s⟩ := hx _ hkey
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : G
hx : ∀ t ∈ 𝓝 x, (t ∩ U).Nonempty
hkey : (fun (y : G) ↦ x / y) ⁻¹' U ∈ 𝓝 x
a : G
ha_mem : Membership.mem (γ := Set G) ((fun (y : G) ↦ x / y) ⁻¹' U) a
ha_s : a ∈ U
⊢ x ∈ U * U

Tactic:
Set.mem_mul.mpr ⟨x / a, ha_mem, a, ha_s, div_mul_cancel x a⟩

Premises used: Iff.mpr, HDiv.hDiv, And.intro, Exists.intro, div_mul_cancel, Set.mem_mul
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : G
hx : ∀ t ∈ 𝓝 x, (t ∩ U).Nonempty
hkey : (fun (y : G) ↦ x / y) ⁻¹' U ∈ 𝓝 x
a : G
ha_mem : Membership.mem (γ := Set G) ((fun (y : G) ↦ x / y) ⁻¹' U) a
ha_s : a ∈ U
⊢ x ∈ U * U

Tactic:
exact Set.mem_mul.mpr ⟨x / a, ha_mem, a, ha_s, div_mul_cancel x a⟩

Premises used: Iff.mpr, HDiv.hDiv, And.intro, Exists.intro, div_mul_cancel, Set.mem_mul
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
⊢ RegularSpace G

Tactic:
.of_exists_mem_nhds_isClosed_subset fun a s hs ↦ ?_

Premises used: RegularSpace.of_exists_mem_nhds_isClosed_subset
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
refine : ∀ (a : G) (s : Set G) (hs : s ∈ 𝓝 a), ∃ t ∈ 𝓝 a, IsClosed[inst] t ∧ t ⊆ s
⊢ RegularSpace G

Tactic:
refine .of_exists_mem_nhds_isClosed_subset fun a s hs ↦ ?_
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
⊢ Tendsto (fun (p : G × G) ↦ p.1 * p.2) (𝓝 (a, 1)) (𝓝 a)

Tactic:
have : Tendsto (fun p : G × G => p.1 * p.2) (𝓝 (a, 1)) (𝓝 a) :=
    continuous_mul.tendsto' _ _ (mul_one a)
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
this : Tendsto (fun (p : G × G) ↦ p.1 * p.2) (𝓝 (a, 1)) (𝓝 a)
rcases :
  ∀ (U : Set G) (hU : U ∈ 𝓝 a) (V : Set G) (hV : Membership.mem (γ := Filter G) (𝓝 1) V)
    (hUV : U ×ˢ V ⊆ (fun (p : G × G) ↦ p.1 * p.2) ⁻¹' s), ∃ t ∈ 𝓝 a, IsClosed[inst] t ∧ t ⊆ s
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst] t ∧ t ⊆ s

Tactic:
rcases mem_nhds_prod_iff.mp (this hs) with ⟨U, hU, V, hV, hUV⟩

Premises used: mem_nhds_prod_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
this : Tendsto (fun (p : G × G) ↦ p.1 * p.2) (𝓝 (a, 1)) (𝓝 a)
U : Set G
hU : U ∈ 𝓝 a
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V
hUV : U ×ˢ V ⊆ (fun (p : G × G) ↦ p.1 * p.2) ⁻¹' s
⊢ image2 HMul.hMul U V ⊆ s

Tactic:
rw [← image_subset_iff, image_prod] at hUV

Premises used: Set.image_prod, Set.image_subset_iff
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
this : Tendsto (fun (p : G × G) ↦ p.1 * p.2) (𝓝 (a, 1)) (𝓝 a)
U : Set G
hU : U ∈ 𝓝 a
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V
hUV : image2 HMul.hMul U V ⊆ s
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst] t ∧ t ⊆ s

Tactic:
⟨closure U, mem_of_superset hU subset_closure, isClosed_closure, ?_⟩

Premises used: subset_closure, closure, And.intro, Exists.intro, isClosed_closure, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
this : Tendsto (fun (p : G × G) ↦ p.1 * p.2) (𝓝 (a, 1)) (𝓝 a)
U : Set G
hU : U ∈ 𝓝 a
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V
hUV : image2 HMul.hMul U V ⊆ s
refine : closure[inst] U ⊆ s
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst] t ∧ t ⊆ s

Tactic:
refine ⟨closure U, mem_of_superset hU subset_closure, isClosed_closure, ?_⟩
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
this : Tendsto (fun (p : G × G) ↦ p.1 * p.2) (𝓝 (a, 1)) (𝓝 a)
U : Set G
hU : U ∈ 𝓝 a
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V
hUV : image2 HMul.hMul U V ⊆ s
⊢ closure[inst] U ⊆ closure[inst] U * interior V

Tactic:
subset_mul_left _ (mem_interior_iff_mem_nhds.2 hV)

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, Set.subset_mul_left
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
this : Tendsto (fun (p : G × G) ↦ p.1 * p.2) (𝓝 (a, 1)) (𝓝 a)
U : Set G
hU : U ∈ 𝓝 a
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V
hUV : image2 HMul.hMul U V ⊆ s
⊢ closure[inst] U * interior V = U * interior V

Tactic:
isOpen_interior.closure_mul U

Premises used: isOpen_interior, IsOpen.closure_mul