mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
X : Type u_5
inst✝¹ : TopologicalSpace X
M : Type u_6
inst✝ : One M
f : ι → X → M
hf : LocallyFinite fun i ↦ mulSupport (f i)
x₀ : X
⊢ ∃ I, ∀ᶠ (x : X) in 𝓝 x₀, (mulSupport fun i ↦ f i x) ⊆ ↑I

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous[inst✝³, inst✝²] (f i)
hf : LocallyFinite fun i ↦ mulSupport (f i)
⊢ Continuous[inst✝³, inst✝²] fun x ↦ ∏ᶠ (i : ι), f i x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
p : ι → Prop
hc : ∀ (i : ι), p i → Continuous[inst✝³, inst✝²] (f i)
hf : LocallyFinite fun i ↦ mulSupport (f i)
⊢ Continuous[inst✝³, inst✝²] fun x ↦ ∏ᶠ (i : ι) (_ : p i), f i x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: M : Type u_1
s : Set M
inst✝³ : Mul M
inst✝² : TopologicalSpace M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
m : M
⊢ IsOpen[inst✝²] {x | m ∈ s}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
ι' : Sort u_6
inst✝ : Mul M
ts : ι' → TopologicalSpace M
h' : ∀ (i : ι'), ContinuousMul M
⊢ ContinuousMul M

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : Continuous[inst✝¹, inst✝] f
f_inj : Injective f
⊢ IsProperMap f ↔ IsClosedMap f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: M : Type u_1
s : Set M
inst✝³ : Mul M
inst✝² : TopologicalSpace M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
⊢ IsClosed[inst✝²] s.centralizer

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
a : G
⊢ (Homeomorph.mulLeft a).symm = Homeomorph.mulLeft a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: X : Type u_6
inst✝² : Semigroup X
inst✝¹ : TopologicalSpace X
inst✝ : SeparatelyContinuousMul X
x y : X
⊢ ContinuousMap.mulRight (x * y) = (ContinuousMap.mulRight y).comp (ContinuousMap.mulRight x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: X : Type u_6
inst✝² : Semigroup X
inst✝¹ : TopologicalSpace X
inst✝ : SeparatelyContinuousMul X
x y : X
⊢ ContinuousMap.mulLeft (x * y) = (ContinuousMap.mulLeft x).comp (ContinuousMap.mulLeft y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : T1Space Y
⊢ IsProperMap f ↔ Continuous[inst✝², inst✝¹] f ∧ IsClosedMap f ∧ Tendsto f (cocompact X) cofinite

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
hf : Continuous[inst✝³, inst✝²] f
⊢ Tendsto f (cocompact X) cofinite

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
c a : G
⊢ map (fun x ↦ c * x) (𝓝[≠] a) = 𝓝[≠] (c * a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
h : ∀ (y_1 : Y), IsCompact ((fun x ↦ y) ⁻¹' {y_1})
⊢ IsCompact univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
a : G
⊢ (Homeomorph.mulRight a).symm = Homeomorph.mulRight a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
c a : G
⊢ map (fun x ↦ x * c) (𝓝[≠] a) = 𝓝[≠] (a * c)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
⊢ (IsProperMap fun x ↦ y) ↔ CompactSpace X

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
β : Type v
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed[inst✝⁴] t
hs : IsCompact s
x✝ : ↑s × β
⊢ (fun gx ↦ (gx.1, (↑gx.1)⁻¹ • gx.2)) ((fun gx ↦ (gx.1, ↑gx.1 • gx.2)) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
β : Type v
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed[inst✝⁴] t
hs : IsCompact s
x✝ : ↑s × β
⊢ (fun gx ↦ (gx.1, ↑gx.1 • gx.2)) ((fun gx ↦ (gx.1, (↑gx.1)⁻¹ • gx.2)) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
β : Type v
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed[inst✝⁴] t
hs : IsCompact s
⊢ IsClosed[inst✝⁴] (s • t)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
g h : G
⊢ ∀ (y : G), IsConnected (⇑(Homeomorph.mulLeft g) ⁻¹' {y})

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Quotient

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
s : Set G
⊢ Dense (mk '' s) ↔ Dense (s * ↑N)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Quotient

Goal state before:
pp: G✝ : Type u_1
inst✝⁵ : TopologicalSpace G✝
inst✝⁴ : Group G✝
inst✝³ : SeparatelyContinuousMul G✝
N✝ : Subgroup G✝
G : Type u_2
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
N : Subgroup G
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace N] fun p ↦ p.1 • p.2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Quotient

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
γ : G
⊢ Continuous[instTopologicalSpace N, instTopologicalSpace N] fun x ↦ γ • x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Quotient

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
⊢ T1Space (G ⧸ N) ↔ IsClosed[inst✝²] ↑N

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
β : Type v
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
inst✝ : CompactSpace α
⊢ IsClosedMap Quotient.mk'

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
h : connectedComponent 1 = {1}
g : G
⊢ connectedComponent g = {g}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul α α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ {a} * s ∈ 𝓝 (a * b)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul α α
s : Set α
a : α
h : s ∈ 𝓝 1
⊢ {a} * s ∈ 𝓝 a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Quotient

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
N : Subgroup G
⊢ DiscreteTopology (G ⧸ N) ↔ IsOpen[inst✝²] ↑N

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
hs : IsOpen[inst✝²] s
⊢ IsOpen[inst✝²] (s * t)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Quotient

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
N : Subgroup G
inst✝ : N.Normal
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace N] fun p ↦ p.1 * p.2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ s * {a} ∈ 𝓝 (b * a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s : Set α
a : α
h : s ∈ 𝓝 1
⊢ s * {a} ∈ 𝓝 a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun x ↦ f x * b) l (𝓝 (c * b)) ↔ Tendsto f l (𝓝 c)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
s s' : Set G
hs₀ : s ∈ 𝓝 1
h_symm : ∀ x ∈ s, x⁻¹ ∈ s
y : G
hy : y ∈ closure[inst✝²] s'
⊢ (fun x ↦ x * y) '' s ∈ 𝓝 y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Quotient

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : Subgroup G
hH : IsCompact ↑H
⊢ IsClosedMap mk

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
s s' : Set G
hs₀ : s ∈ 𝓝 1
h_symm : ∀ x ∈ s, x⁻¹ ∈ s
⊢ closure[inst✝²] s' ⊆ s * s'

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Quotient

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
N : Subgroup G
inst✝ : N.Normal
hN : IsClosed[inst✝³] ↑N
⊢ T3Space (G ⧸ N)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
s s' : Set G
hs'₀ : s' ∈ 𝓝 1
h_symm : ∀ x ∈ s', x⁻¹ ∈ s'
y : G
hy : y ∈ closure[inst✝²] s
⊢ (fun x ↦ y * x) '' s' ∈ 𝓝 y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
s s' : Set G
hs'₀ : s' ∈ 𝓝 1
h_symm : ∀ x ∈ s', x⁻¹ ∈ s'
⊢ closure[inst✝²] s ⊆ s * s'

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
ht : IsOpen[inst✝²] t
⊢ IsOpen[inst✝²] (s / t)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
hs : IsOpen[inst✝²] s
⊢ IsOpen[inst✝²] (s / t)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : IsOpen[inst✝²] s
t : Set G
⊢ s * closure[inst✝²] t = s * t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun x ↦ b * f x) l (𝓝 (b * c)) ↔ Tendsto f l (𝓝 c)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : IsOpen[inst✝²] t
s : Set G
⊢ closure[inst✝²] s * t = s * t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : MonoidHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousInv β
f : F
⊢ ContinuousInv α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : IsOpen[inst✝²] s
t : Set G
⊢ s / closure[inst✝²] t = s / t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : IsOpen[inst✝²] t
s : Set G
⊢ closure[inst✝²] s / t = s / t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : DivInvMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
inst✝ : ContinuousInv G
x y : G
h : x ⤳ y
n : ℕ
⊢ (x ^ Int.ofNat n) ⤳ (y ^ Int.ofNat n)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
ht : IsClosed[inst✝²] t
hs : IsCompact s
⊢ IsClosed[inst✝²] (t * s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : DivInvMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
inst✝ : ContinuousInv G
x y : G
h : x ⤳ y
n : ℕ
⊢ (x ^ Int.negSucc n) ⤳ (y ^ Int.negSucc n)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type u_1
inst✝¹ : MulOneClass G
inst✝ : TopologicalSpace G
s : Set G
⊢ s ⊆ s * {1}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type u_1
inst✝¹ : MulOneClass G
inst✝ : TopologicalSpace G
s : Set G
⊢ s ⊆ s * closure[inst✝] {1}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G₁ : Type u_2
G₂ : Type u_3
inst✝⁴ : TopologicalSpace G₂
inst✝³ : T2Space G₂
inst✝² : Inv G₁
inst✝¹ : Inv G₂
inst✝ : ContinuousInv G₂
⊢ IsClosed[Pi.topologicalSpace] {f | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ closure[inst✝²] (K * {1}) = closure[inst✝²] K

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : InvolutiveInv G
inst✝ : ContinuousInv G
l : Filter α
m : α → G
a : G
h : Tendsto (fun x ↦ (m x)⁻¹) l (𝓝 a⁻¹)
⊢ Tendsto m l (𝓝 a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : InvolutiveInv G
inst✝ : ContinuousInv G
s : Set G
hs : IsCompact s
⊢ IsCompact s⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ K * closure[inst✝²] {1} = closure[inst✝²] K

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
F : Set G
hF : IsClosed[inst✝²] F
⊢ F * closure[inst✝²] {1} = closure[inst✝²] F * closure[inst✝²] {1}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : InvolutiveInv G
inst✝ : ContinuousInv G
a : G
⊢ (𝓝[≠] a)⁻¹ = 𝓝[≠] a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
F : Set G
hF : IsClosed[inst✝²] F
⊢ closure[inst✝²] (F * {1}) = F

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
F : Set G
hF : IsClosed[inst✝²] F
⊢ F * closure[inst✝²] {1} = F

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
ι' : Sort u_1
inst✝ : Inv G
ts' : ι' → TopologicalSpace G
h' : ∀ (i : ι'), ContinuousInv G
⊢ ContinuousInv G

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure[inst✝²] {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:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

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

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁴ : Inv G
inst✝³ : Inv H
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace H
inst✝ : ContinuousInv H
f : G → H
hf : IsInducing f
hf_inv : ∀ (x : G), f x⁻¹ = (f x)⁻¹
⊢ Continuous[inst✝², inst✝¹] (f ∘ fun a ↦ a⁻¹)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : TopologicalSpace G
inst✝² : MulDistribMulAction H G
inst✝¹ : ContinuousConstSMul H G
𝒢 : Subgroup G
h : H
inst✝ : IsDiscrete ↑𝒢
x y : G
⊢ ((MulDistribMulAction.toMonoidEnd H G) h) x = ((MulDistribMulAction.toMonoidEnd H G) h) y → x = y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : t * closure[inst✝²] {1} = t
⊢ tᶜ * closure[inst✝²] {1} = tᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : 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

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
h : tᶜ * closure[inst✝²] {1} = tᶜ
⊢ t * closure[inst✝²] {1} = t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: Gᵣ : Type u_3
inst✝² : UniformSpace Gᵣ
inst✝¹ : Group Gᵣ
inst✝ : IsRightUniformGroup Gᵣ
⊢ 𝓤 Gᵣ = comap (fun x ↦ x.1 * x.2⁻¹) (𝓝 1)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: Gₗ : Type u_2
inst✝² : UniformSpace Gₗ
inst✝¹ : Group Gₗ
inst✝ : IsLeftUniformGroup Gₗ
⊢ comap Prod.swap (𝓤 Gₗ) = comap (fun x ↦ x.2⁻¹ * x.1) (𝓝 1)

Tactic:
uniformity_eq_comap_inv_mul_nhds_one,

Goal state after:
Gₗ : Type u_2
inst✝² : UniformSpace Gₗ
inst✝¹ : Group Gₗ
inst✝ : IsLeftUniformGroup Gₗ
⊢ comap Prod.swap (comap (fun x ↦ x.1⁻¹ * x.2) (𝓝 1)) = comap (fun x ↦ x.2⁻¹ * x.1) (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : TopologicalSpace G
inst✝² : MulDistribMulAction H G
inst✝¹ : ContinuousConstSMul H G
𝒢 : Subgroup G
h : H
inst✝ : DiscreteTopology ↥𝒢
⊢ DiscreteTopology ↥(h • 𝒢)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
n : ℕ
⊢ Continuous[inst✝², inst✝²] fun a ↦ a ^ Int.ofNat n

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
x : G
hx : ∀ t ∈ 𝓝 x, (t ∩ U).Nonempty
⊢ ContinuousAt (fun y ↦ x / y) x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
n : ℕ
⊢ Continuous[inst✝², inst✝²] fun a ↦ a ^ Int.negSucc n

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: Gₗ : Type u_2
inst✝² : UniformSpace Gₗ
inst✝¹ : Group Gₗ
inst✝ : IsLeftUniformGroup Gₗ
⊢ 𝓤 Gₗ = comap (fun x ↦ x.2⁻¹ * x.1) (𝓝 1)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
x : G
hx : ∀ t ∈ 𝓝 x, (t ∩ U).Nonempty
⊢ U ∈ 𝓝 (x / x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousMul H
c a : H
⊢ map (fun x ↦ c * x) (𝓝[>] a) = 𝓝[>] (c * a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: Gᵣ : Type u_3
inst✝² : UniformSpace Gᵣ
inst✝¹ : Group Gᵣ
inst✝ : IsRightUniformGroup Gᵣ
⊢ 𝓤 Gᵣ = comap (fun x ↦ x.2 / x.1) (𝓝 1)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
⊢ closure[inst✝²] U ⊆ U * U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousMul H
c a : H
⊢ map (fun x ↦ c * x) (𝓝[<] a) = 𝓝[<] (c * a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: Gᵣ : Type u_3
inst✝² : UniformSpace Gᵣ
inst✝¹ : Group Gᵣ
inst✝ : IsRightUniformGroup Gᵣ
⊢ 𝓤 Gᵣ = comap (fun x ↦ x.1 / x.2) (𝓝 1)

Tactic:
by

Goal state after: