awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : CompactSpace M
inst_4 : T1Space M
U : Set M
hU : IsOpen[inst_1] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : univ * W ⊆ U
pos : ∀ (H : ∃ (x : M), x ≠ 0 ∧ x ∈ W), IsOpen[inst_1] {0}
neg : ∀ (H : ¬∃ (x : M), x ≠ 0 ∧ x ∈ W), IsOpen[inst_1] {0}
⊢ IsOpen[inst_1] {0}

Tactic:
by_cases H : ∃ x ≠ 0, x ∈ W
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : CompactSpace M
inst_4 : T1Space M
U : Set M
hU : IsOpen[inst_1] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : univ * W ⊆ U
H : ∃ (x : M), x ≠ 0 ∧ x ∈ W
pos : ∀ (x : M) (hx : x ≠ 0) (hxW : x ∈ W), IsOpen[inst_1] {0}
⊢ IsOpen[inst_1] {0}

Tactic:
obtain ⟨x, hx, hxW⟩ := H
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : CompactSpace M
inst_4 : T1Space M
U : Set M
hU : IsOpen[inst_1] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : univ * W ⊆ U
x : M
hx : x ≠ 0
hxW : x ∈ W
⊢ 1 ∈ univ * W

Tactic:
simpa [hx] using Set.mul_mem_mul (Set.mem_univ x⁻¹) hxW

Premises used: Inv.inv, Set.mem_univ, Set.mul_mem_mul
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : CompactSpace M
inst_4 : T1Space M
U : Set M
hU : IsOpen[inst_1] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : univ * W ⊆ U
x : M
hx : x ≠ 0
hxW : x ∈ W
⊢ IsOpen[inst_1] {0}

Tactic:
cases h1U (hW' (by simpa [hx] using Set.mul_mem_mul (Set.mem_univ x⁻¹) hxW))
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : CompactSpace M
inst_4 : T1Space M
U : Set M
hU : IsOpen[inst_1] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : univ * W ⊆ U
H : ¬∃ (x : M), x ≠ 0 ∧ x ∈ W
⊢ W ⊆ {0}

Tactic:
simpa [not_imp_not] using H

Premises used: not_imp_not
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : CompactSpace M
inst_4 : T1Space M
U : Set M
hU : IsOpen[inst_1] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : univ * W ⊆ U
H : ¬∃ (x : M), x ≠ 0 ∧ x ∈ W
⊢ {0} ⊆ W

Tactic:
simpa using mem_of_mem_nhds hW

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : CompactSpace M
inst_4 : T1Space M
U : Set M
hU : IsOpen[inst_1] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : univ * W ⊆ U
H : ¬∃ (x : M), x ≠ 0 ∧ x ∈ W
⊢ Membership.mem (γ := Filter M) (𝓝 0) {0}

Tactic:
obtain rfl : W = {0} := subset_antisymm
      (by simpa [not_imp_not] using H) (by simpa using mem_of_mem_nhds hW)

Premises used: subset_antisymm, rfl
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : CompactSpace M
inst_4 : T1Space M
U : Set M
hU : IsOpen[inst_1] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : univ * W ⊆ U
H : ¬∃ (x : M), x ≠ 0 ∧ x ∈ W
hW₁ : Membership.mem (γ := Filter M) (𝓝 0) {0}
⊢ HMul.hMul (α := Set M) univ {0} ⊆ U

Tactic:
obtain rfl : W = {0} := subset_antisymm
      (by simpa [not_imp_not] using H) (by simpa using mem_of_mem_nhds hW)

Premises used: subset_antisymm, rfl
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : CompactSpace M
inst_4 : T1Space M
U : Set M
hU : IsOpen[inst_1] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : Membership.mem (γ := Filter M) (𝓝 0) W
hW' : univ * W ⊆ U
H : ¬∃ (x : M), x ≠ 0 ∧ x ∈ W
hW₁ : Membership.mem (γ := Filter M) (𝓝 0) {0}
hW'₁ : HMul.hMul (α := Set M) univ {0} ⊆ U
⊢ ¬∃ (x : M), x ≠ 0 ∧ Membership.mem (γ := Set M) {0} x

Tactic:
obtain rfl : W = {0} := subset_antisymm
      (by simpa [not_imp_not] using H) (by simpa using mem_of_mem_nhds hW)

Premises used: subset_antisymm, rfl
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
inst_3 : CompactSpace M
inst_4 : T1Space M
U : Set M
hU : IsOpen[inst_1] U
h0U : 0 ∈ U
h1U : 1 ∉ U
hW : Membership.mem (γ := Filter M) (𝓝 0) {0}
hW' : HMul.hMul (α := Set M) univ {0} ⊆ U
H : ¬∃ (x : M), x ≠ 0 ∧ Membership.mem (γ := Set M) {0} x
⊢ IsOpen[inst_1] {0}

Tactic:
simpa [isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulOneClass M
inst_2 : ContinuousMul M
s : Set M
hs : Membership.mem (γ := Filter M) (𝓝 1) s
⊢ s ∈ 𝓝 (HMul.hMul (α := M) 1 1)

Tactic:
simpa only [one_mul] using hs

Premises used: one_mul
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulOneClass M
inst_2 : ContinuousMul M
s : Set M
hs : Membership.mem (γ := Filter M) (𝓝 1) s
⊢ Membership.mem (γ := Filter (M × M)) (𝓝 (1, 1)) ((fun (a : M × M) ↦ a.1 * a.2) ⁻¹' s)

Tactic:
have : (fun a : M × M => a.1 * a.2) ⁻¹' s ∈ 𝓝 ((1, 1) : M × M) :=
    tendsto_mul (by simpa only [one_mul] using hs)
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulOneClass M
inst_2 : ContinuousMul M
s : Set M
hs : Membership.mem (γ := Filter M) (𝓝 1) s
this : Membership.mem (γ := Filter (M × M)) (𝓝 (1, 1)) ((fun (a : M × M) ↦ a.1 * a.2) ⁻¹' s)
⊢ ∃ (V : Set M), IsOpen[inst] V ∧ 1 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s

Tactic:
simpa only [prod_subset_iff] using exists_nhds_square this

Premises used: exists_nhds_square, Set.prod_subset_iff
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulOneClass M
inst_2 : ContinuousMul M
s : Set M
hs : Membership.mem (γ := Filter M) (𝓝 1) s
⊢ ∃ (V : Set M), Membership.mem (γ := Filter M) (𝓝 1) V ∧ ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s

Tactic:
let ⟨V, Vo, V1, hV⟩ := exists_open_nhds_one_split hs
  ⟨V, IsOpen.mem_nhds Vo V1, hV⟩

Premises used: _private.0.exists_nhds_one_split.match_1, Membership.mem, Exists, nhds, And, exists_open_nhds_one_split, And.intro, IsOpen.mem_nhds, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulOneClass M
inst_2 : ContinuousMul M
U : Set M
hU : Membership.mem (γ := Filter M) (𝓝 1) U
⊢ ∃ (V : Set M), IsOpen[inst] V ∧ 1 ∈ V ∧ V * V ⊆ U

Tactic:
simpa only [mul_subset_iff] using exists_open_nhds_one_split hU

Premises used: Set.mul_subset_iff, exists_open_nhds_one_split
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulOneClass M
inst_2 : ContinuousMul M
p : ι → Prop
s : ι → Set M
h : HasBasis (𝓝 1) p s
rw :
  HasBasis (α := M)
    (Filter.map (Function.uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
    p fun (i : ι) ↦ s i * s i
⊢ HasBasis.{u_3, u_1 + 1} (α := M) (𝓝 1) p fun (i : ι) ↦ s i * s i

Tactic:
rw [← nhds_mul_nhds_one, ← map₂_mul, ← map_uncurry_prod]

Premises used: nhds_mul_nhds_one, Filter.map₂_mul, Filter.map_uncurry_prod
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
M : Type u_3
inst : TopologicalSpace M
inst_1 : MulOneClass M
inst_2 : ContinuousMul M
p : ι → Prop
s : ι → Set M
h : HasBasis (𝓝 1) p s
⊢ HasBasis (α := M)
    (Filter.map (Function.uncurry fun (x1 x2 : M) ↦ x1 * x2) (SProd.sprod (α := Filter M) (β := Filter M) (𝓝 1) (𝓝 1)))
    p fun (i : ι) ↦ s i * s i

Tactic:
simpa only [← image_mul_prod] using h.prod_self.map _

Premises used: Filter.HasBasis.prod_self, Set.image_mul_prod, Filter.HasBasis.map
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Semigroup M
inst_2 : SeparatelyContinuousMul M
s : Subsemigroup M
⊢ closure[inst] (↑s : Set M) * closure[inst] (↑s : Set M) ⊆ closure[inst] (↑s : Set M)

Tactic:
image2_subset_iff.2 fun _ hx _ hy =>
    map_mem_closure₂' continuous_const_mul continuous_mul_const
      hx hy fun _ ha _ hb => s.mul_mem ha hb

Premises used: Iff.mpr, Subsemigroup.mul_mem, continuous_const_mul, Set.image2_subset_iff, map_mem_closure₂', continuous_mul_const
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Semigroup M
inst_2 : SeparatelyContinuousMul M
s : Subsemigroup M
⊢ (↑s.topologicalClosure : Set M) = closure[inst] (↑s : Set M)

Tactic:
rfl

Premises used: setOf, closure, Set.sInter, rfl
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Semigroup M
inst_2 : SeparatelyContinuousMul M
s : Subsemigroup M
⊢ s ≤ s.topologicalClosure

Tactic:
_root_.subset_closure

Premises used: Set.Mem, subset_closure, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Semigroup M
inst_2 : SeparatelyContinuousMul M
s : Subsemigroup M
⊢ IsClosed[inst] (↑s.topologicalClosure : Set M)

Tactic:
isClosed_closure

Premises used: setOf, closure, isClosed_closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Semigroup M
inst_2 : SeparatelyContinuousMul M
s t : Subsemigroup M
h : s ≤ t
ht : IsClosed[inst] (↑t : Set M)
⊢ s.topologicalClosure ≤ t

Tactic:
closure_minimal h ht

Premises used: Set.Mem, closure_minimal, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Semigroup M
inst_2 : SeparatelyContinuousMul M
s t : Subsemigroup M
h : s ≤ t
⊢ s.topologicalClosure ≤ t.topologicalClosure

Tactic:
_root_.closure_mono h

Premises used: Set.Mem, setOf, closure_mono, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Semigroup M
inst_3 : SeparatelyContinuousMul M
inst_4 : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x_1 x_2 : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ s.topologicalClosure) x hx *
          Subtype.mk (p := fun (x : M) ↦ x ∈ s.topologicalClosure) y hy) :
      M) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ s.topologicalClosure) y hy *
          Subtype.mk (p := fun (x : M) ↦ x ∈ s.topologicalClosure) x hx) :
      M)

Tactic:
eqOn_closure₂' this ?_ ?_ ?_ ?_ x hx y hy

Premises used: eqOn_closure₂'
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Semigroup M
inst_3 : SeparatelyContinuousMul M
inst_4 : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x_1 x_2 : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
refine_1 : ∀ (x : M), Continuous[inst_1, inst_1] (HMul.hMul x)
refine_2 refine_3 : ∀ (x : M), Continuous[inst_1, inst_1] fun (y : M) ↦ y * x
refine_4 : ∀ (y : M), Continuous[inst_1, inst_1] fun (x : M) ↦ y * x
⊢ (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ s.topologicalClosure) x hx *
          Subtype.mk (p := fun (x : M) ↦ x ∈ s.topologicalClosure) y hy) :
      M) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ s.topologicalClosure) y hy *
          Subtype.mk (p := fun (x : M) ↦ x ∈ s.topologicalClosure) x hx) :
      M)

Tactic:
refine eqOn_closure₂' this ?_ ?_ ?_ ?_ x hx y hy

Premises used: eqOn_closure₂'
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Semigroup M
inst_3 : SeparatelyContinuousMul M
inst_4 : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x_1 x_2 : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ ∀ (x : M), Continuous[inst_1, inst_1] (HMul.hMul x)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Semigroup M
inst_3 : SeparatelyContinuousMul M
inst_4 : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x_1 x_2 : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ ∀ (y : M), Continuous[inst_1, inst_1] fun (x : M) ↦ x * y

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Semigroup M
inst_3 : SeparatelyContinuousMul M
inst_4 : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x_1 x_2 : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ ∀ (x : M), Continuous[inst_1, inst_1] fun (y : M) ↦ y * x

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace M
inst_2 : Semigroup M
inst_3 : SeparatelyContinuousMul M
inst_4 : T2Space M
s : Subsemigroup M
hs : ∀ (x y : ↥s), x * y = y * x
this : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
x_1 x_2 : ↥s.topologicalClosure
x : M
hx : x ∈ s.topologicalClosure
y : M
hy : y ∈ s.topologicalClosure
⊢ ∀ (y : M), Continuous[inst_1, inst_1] fun (x : M) ↦ y * x

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
N : Type u_4
inst : TopologicalSpace N
inst_1 : Mul N
inst_2 : ContinuousMul N
s t : Set N
hs : IsCompact s
ht : IsCompact t
rw : IsCompact (X := N) ((fun (x : N × N) ↦ x.1 * x.2) '' s ×ˢ t)
⊢ IsCompact (s * t)

Tactic:
rw [← image_mul_prod]

Premises used: Set.image_mul_prod
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
N : Type u_4
inst : TopologicalSpace N
inst_1 : Mul N
inst_2 : ContinuousMul N
s t : Set N
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (X := N) ((fun (x : N × N) ↦ x.1 * x.2) '' s ×ˢ t)

Tactic:
(hs.prod ht).image continuous_mul

Premises used: IsCompact.prod, continuous_mul, IsCompact.image
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
N : Type u_4
inst : TopologicalSpace N
inst_1 : Mul N
inst_2 : ContinuousMul N
s t : Set N
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (X := N) ((fun (x : N × N) ↦ x.1 * x.2) '' s ×ˢ t)

Tactic:
exact (hs.prod ht).image continuous_mul

Premises used: IsCompact.prod, continuous_mul, IsCompact.image
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
s : Submonoid M
⊢ closure[inst] (↑s : Set M) * closure[inst] (↑s : Set M) ⊆ closure[inst] (↑s : Set M)

Tactic:
image2_subset_iff.2 fun _ hx _ hy =>
    map_mem_closure₂' continuous_const_mul continuous_mul_const hx hy
      fun _ ha _ hb ↦ s.mul_mem ha hb

Premises used: Iff.mpr, Submonoid.mul_mem, continuous_const_mul, Set.image2_subset_iff, map_mem_closure₂', continuous_mul_const
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
s : Submonoid M
⊢ closure[inst] (↑s : Set M) * closure[inst] (↑s : Set M) = closure[inst] (↑s : Set M)

Tactic:
Subset.antisymm s.top_closure_mul_self_subset fun x hx =>
    ⟨x, hx, 1, _root_.subset_closure s.one_mem, mul_one _⟩

Premises used: Set.Subset.antisymm, Submonoid.top_closure_mul_self_subset, subset_closure, Submonoid.one_mem, And.intro, Exists.intro, mul_one, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
s : Submonoid M
⊢ (↑s.topologicalClosure : Set M) = closure[inst] (↑s : Set M)

Tactic:
rfl

Premises used: setOf, closure, Set.sInter, rfl
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
s : Submonoid M
⊢ s ≤ s.topologicalClosure

Tactic:
_root_.subset_closure

Premises used: Set.Mem, subset_closure, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
s : Submonoid M
⊢ IsClosed[inst] (↑s.topologicalClosure : Set M)

Tactic:
isClosed_closure

Premises used: setOf, closure, isClosed_closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
s t : Submonoid M
h : s ≤ t
ht : IsClosed[inst] (↑t : Set M)
⊢ s.topologicalClosure ≤ t

Tactic:
closure_minimal h ht

Premises used: Set.Mem, closure_minimal, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
s t : Submonoid M
h : s ≤ t
⊢ s.topologicalClosure ≤ t.topologicalClosure

Tactic:
_root_.closure_mono h

Premises used: Set.Mem, setOf, closure_mono, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto (fun (x : M) ↦ a * x) (cocompact M) (cocompact M)

Tactic:
Filter.Tendsto.of_tendsto_comp ?_ (Filter.comap_cocompact_le (continuous_const_mul b))

Premises used: Filter.comap_cocompact_le, continuous_const_mul, Filter.Tendsto.of_tendsto_comp
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
a b : M
ha : b * a = 1
refine : Tendsto ((fun (x : M) ↦ b * x) ∘ fun (x : M) ↦ a * x) (cocompact M) (cocompact M)
⊢ Tendsto (fun (x : M) ↦ a * x) (cocompact M) (cocompact M)

Tactic:
refine Filter.Tendsto.of_tendsto_comp ?_ (Filter.comap_cocompact_le (continuous_const_mul b))

Premises used: Filter.comap_cocompact_le, continuous_const_mul, Filter.Tendsto.of_tendsto_comp
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto id (cocompact M) (cocompact M)

Tactic:
Filter.tendsto_id

Premises used: Filter.tendsto_id
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
a b : M
ha : b * a = 1
h : Eq.{u_3 + 1} (α := M → M) ((fun (x : M) ↦ b * x) ∘ fun (x : M) ↦ a * x) id
⊢ Tendsto ((fun (x : M) ↦ b * x) ∘ fun (x : M) ↦ a * x) (cocompact M) (cocompact M)

Tactic:
convert! Filter.tendsto_id

Premises used: Filter.tendsto_id
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
a b : M
ha : b * a = 1
h : ∀ (x : M), ((fun (x : M) ↦ b * x) ∘ fun (x : M) ↦ a * x) x = id x
⊢ Eq.{u_3 + 1} (α := M → M) ((fun (x : M) ↦ b * x) ∘ fun (x : M) ↦ a * x) id

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
a b : M
ha : b * a = 1
x : M
⊢ ((fun (x : M) ↦ b * x) ∘ fun (x : M) ↦ a * x) x = id x

Tactic:
simp [← mul_assoc, ha]

Premises used: mul_assoc
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto (fun (x : M) ↦ x * a) (cocompact M) (cocompact M)

Tactic:
Filter.Tendsto.of_tendsto_comp ?_ (Filter.comap_cocompact_le (continuous_mul_const b))

Premises used: Filter.comap_cocompact_le, Filter.Tendsto.of_tendsto_comp, continuous_mul_const
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
a b : M
ha : a * b = 1
refine : Tendsto ((fun (x : M) ↦ x * b) ∘ fun (x : M) ↦ x * a) (cocompact M) (cocompact M)
⊢ Tendsto (fun (x : M) ↦ x * a) (cocompact M) (cocompact M)

Tactic:
refine Filter.Tendsto.of_tendsto_comp ?_ (Filter.comap_cocompact_le (continuous_mul_const b))

Premises used: Filter.comap_cocompact_le, Filter.Tendsto.of_tendsto_comp, continuous_mul_const
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
a b : M
ha : a * b = 1
simp : Tendsto (fun (x : M) ↦ x) (cocompact M) (cocompact M)
⊢ Tendsto ((fun (x : M) ↦ x * b) ∘ fun (x : M) ↦ x * a) (cocompact M) (cocompact M)

Tactic:
simp only [comp_mul_right, ha, mul_one]

Premises used: comp_mul_right, mul_one
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto (fun (x : M) ↦ x) (cocompact M) (cocompact M)

Tactic:
Filter.tendsto_id

Premises used: Filter.tendsto_id
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : SeparatelyContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto (fun (x : M) ↦ x) (cocompact M) (cocompact M)

Tactic:
exact Filter.tendsto_id

Premises used: Filter.tendsto_id
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
u : Set M
hu : Membership.mem (γ := Filter M) (𝓝 1) u
rcases :
  ∀ (W : Set M) (W1 : Membership.mem (γ := Filter M) (𝓝 1) W) (h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u),
    ∃ (V : Set M),
      Membership.mem (γ := Filter M) (𝓝 1) V ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
⊢ ∃ (V : Set M),
    Membership.mem (γ := Filter M) (𝓝 1) V ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u

Tactic:
rcases exists_nhds_one_split hu with ⟨W, W1, h⟩

Premises used: exists_nhds_one_split
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
u : Set M
hu : Membership.mem (γ := Filter M) (𝓝 1) u
W : Set M
W1 : Membership.mem (γ := Filter M) (𝓝 1) W
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
rcases :
  ∀ (V : Set M) (V1 : Membership.mem (γ := Filter M) (𝓝 1) V) (h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W),
    ∃ (V : Set M),
      Membership.mem (γ := Filter M) (𝓝 1) V ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
⊢ ∃ (V : Set M),
    Membership.mem (γ := Filter M) (𝓝 1) V ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u

Tactic:
rcases exists_nhds_one_split W1 with ⟨V, V1, h'⟩

Premises used: exists_nhds_one_split
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
u : Set M
hu : Membership.mem (γ := Filter M) (𝓝 1) u
W : Set M
W1 : Membership.mem (γ := Filter M) (𝓝 1) W
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
V : Set M
V1 : Membership.mem (γ := Filter M) (𝓝 1) V
h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W
right : ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
⊢ ∃ (V : Set M),
    Membership.mem (γ := Filter M) (𝓝 1) V ∧ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u

Tactic:
use V, V1
-- Module: Mathlib.Topology.Algebra.Monoid
Goal:
M : Type u_3
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : ContinuousMul M
u : Set M
hu : Membership.mem (γ := Filter M) (𝓝 1) u
W : Set M
W1 : Membership.mem (γ := Filter M) (𝓝 1) W
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
V : Set M
V1 : Membership.mem (γ := Filter M) (𝓝 1) V
h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W
v w s t : M
v_in : v ∈ V
w_in : w ∈ V
s_in : s ∈ V
t_in : t ∈ V
⊢ v * w * s * t ∈ u

Tactic:
simpa only [mul_assoc] using h _ (h' v v_in w w_in) _ (h' s s_in t t_in)

Premises used: mul_assoc