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

Goal state before:
pp: α : Type u_3
inst✝¹ : UniformSpace α
inst✝ : Group α
h₁ : UniformContinuous fun p ↦ p.1 * p.2
h₂ : UniformContinuous fun p ↦ p⁻¹
⊢ UniformContinuous fun p ↦ p.1 / p.2

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 ↦ x * c) (𝓝[>] a) = 𝓝[>] (a * c)

Tactic:
by

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

Goal state before:
pp: G : Type w
H : Type x
α : Type u
β : Type v
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
⊢ RegularSpace G

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
⊢ UniformContinuous fun x ↦ (f 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 ↦ x * c) (𝓝[<] a) = 𝓝[<] (a * c)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f g : β → α
hf : UniformContinuous f
hg : UniformContinuous g
⊢ UniformContinuous fun x ↦ f x * g 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
x y : G
⊢ Inseparable x y ↔ x / y ∈ closure[inst✝²] 1

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✝ : ContinuousInv H
a : H
⊢ (𝓝[>] a)⁻¹ = 𝓝[<] a⁻¹

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✝ : ContinuousInv H
a : H
⊢ (𝓝[<] a)⁻¹ = 𝓝[>] a⁻¹

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✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a ↦ a⁻¹) (𝓟 (Ioi a)) (𝓟 (Iio a⁻¹))

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✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a ↦ a⁻¹) (𝓟 (Iio a)) (𝓟 (Ioi a⁻¹))

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✝ : ContinuousInv H
a : H
⊢ Tendsto Inv.inv (𝓝[>] 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
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
x y : G
hspec : x ⤳ y
hne : ¬x = y
⊢ x * y⁻¹ ≠ 1

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✝ : ContinuousInv H
a : H
⊢ Tendsto Inv.inv (𝓝[<] a⁻¹) (𝓝[>] a)

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✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a ↦ a⁻¹) (𝓟 (Ici a)) (𝓟 (Iic a⁻¹))

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✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a ↦ a⁻¹) (𝓟 (Iic a)) (𝓟 (Ici a⁻¹))

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
ι : Type u_5
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : ι → β → α
s : Finset ι
h : ∀ i ∈ s, UniformContinuous (f i)
⊢ UniformContinuous fun x ↦ ∏ i ∈ s, f i 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
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
x y : G
hspec : x ⤳ y
hne : ¬x = y
U : Set G
hU₁ : U ∈ 𝓝 1
hU : x * y⁻¹ ∉ U
⊢ U ∈ 𝓝 (y * y⁻¹)

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✝ : ContinuousInv H
a : H
⊢ Tendsto Inv.inv (𝓝[≥] a⁻¹) (𝓝[≤] a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Type u_3
f g : ι → α × α
l : Filter ι
hf : Tendsto f l (𝓤 α)
hg : Tendsto g l (𝓤 α)
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓤 α ×ˢ 𝓤 α) (𝓤 α)

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
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
⊢ T2Space G

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✝ : ContinuousInv H
a : H
⊢ Tendsto Inv.inv (𝓝[≤] a⁻¹) (𝓝[≥] a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Type u_3
f g : ι → α × α
l : Filter ι
hf : Tendsto f l (𝓤 α)
hg : Tendsto g l (𝓤 α)
⊢ Tendsto (f / g) l (𝓤 α)

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
S : Set G
hS : S ∈ 𝓝 1
⊢ S⁻¹ ∈ 𝓝 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Type u_3
f g : ι → α × α
l : Filter ι
hf : Tendsto f l (𝓤 α)
hfg : Tendsto (f * g) l (𝓤 α)
⊢ Tendsto g l (𝓤 α)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Type u_3
f g : ι → α × α
l : Filter ι
hg : Tendsto g l (𝓤 α)
hfg : Tendsto (f * g) l (𝓤 α)
⊢ Tendsto f l (𝓤 α)

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✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s✝ : Set α
x : α
s : Subgroup G
g : G
hg : g ∈ closure[inst✝³] ↑s
⊢ g⁻¹ ∈ closure[inst✝³] ↑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
U : Set G
hU : U ∈ 𝓝 1
V : Set G
V_open : IsOpen[inst✝²] V
V_mem : 1 ∈ V
hV : V * V ⊆ U
W : Set G
W_mem : W ∈ 𝓝 1
W_closed : IsClosed[inst✝²] W
hW : W ⊆ V
⊢ (W ∩ W⁻¹)⁻¹ = W ∩ W⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
⊢ UniformContinuous fun x ↦ f x ^ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x ↦ f x ^ (n + 1)

Tactic:
simp_rw [pow_succ']
    exact hf.mul (hf.pow_const n)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x ↦ f x ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x ↦ f x ^ ↑n

Tactic:
by

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

Goal state before:
pp: G : Type w
H : Type x
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst✝⁵, inst✝¹] ⇑f
hf' : DenseRange ⇑f
s : Subgroup G
hs : s.topologicalClosure = ⊤
⊢ (Subgroup.map f s).topologicalClosure = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x ↦ f x ^ Int.negSucc n

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
N : Subgroup G
inst✝ : N.Normal
n : G
hn : n ∈ N.topologicalClosure
g : G
⊢ g * n * g⁻¹ ∈ N.topologicalClosure

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
⊢ ∃ V ∈ 𝓝 1, IsClosed[inst✝²] V ∧ V⁻¹ = V ∧ V * V ⊆ U

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
a : α
⊢ 𝓤 α = map (fun x ↦ (x.1 * a, x.2 * a)) (map (fun x ↦ (x.1 * a⁻¹, x.2 * a⁻¹)) (𝓤 α))

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
g h : G
hg : g ∈ connectedComponent 1
hh : h ∈ connectedComponent 1
⊢ (fun x ↦ g * x) 1 = g

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
g h : G
hg : g ∈ connectedComponent 1
hh : h ∈ connectedComponent 1
⊢ g ∈ connectedComponent (g * h)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
g h : G
hg : g ∈ connectedComponent 1
hh : h ∈ connectedComponent 1
⊢ g * h ∈ connectedComponent 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : DivisionMonoid G
inst✝ : ContinuousInv G
g : G
hg : g ∈ connectedComponent 1
⊢ g⁻¹ ∈ connectedComponent 1

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
⊢ ↑⊥.topologicalClosure = 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✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : s ∈ 𝓝 1
⊢ s ∈ 𝓝 ((Prod.fst * Prod.snd⁻¹) (1, 1))

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
s : Set G
hs : s ∈ 𝓝 1
⊢ ∃ V ∈ 𝓝 1, ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s

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
x : G
⊢ map (fun x_1 ↦ x * x_1) (𝓝 1) = 𝓝 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
x : G
⊢ map (fun x_1 ↦ x_1 * x) (𝓝 1) = 𝓝 x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
⊢ 𝓤 α = 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
S : Subgroup G
hS : IsDiscrete ↑S
V : Set G
hV : V ∈ 𝓝 1 ∧ V ∩ ↑S = {1}
U : Set G
hU : U ∈ 𝓝 1
hUinv : U⁻¹ = U
hUV : U * U ⊆ V
g : G
hgS : g ∈ S
x : G
hx : x ∈ U⁻¹
hgx : (fun x ↦ g * x) x ∈ U
⊢ (fun x1 x2 ↦ x1 * x2) ((fun x ↦ g * x) x) x⁻¹ = g

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
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : (𝓝 1).HasBasis p s
x : G
⊢ (𝓝 x).HasBasis p fun i ↦ {y | y / x ∈ s i}

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 : Subgroup G
hS : IsDiscrete ↑S
⊢ ∃ U ∈ 𝓝 1, U⁻¹ = U ∧ ∀ g ∈ S, ((fun x ↦ g * x) '' U ∩ U).Nonempty → g = 1

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
x : G
s : Set G
⊢ x ∈ closure[inst✝²] s ↔ ∀ U ∈ 𝓝 1, ∃ y ∈ s, y / x ∈ U

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
M : Type u_1
hom : Type u_2
inst✝⁴ : MulOneClass M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
f : hom
hf : Tendsto (⇑f) (𝓝 1) (𝓝 1)
x : G
⊢ ContinuousAt (⇑f) 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
M : Type u_1
hom : Type u_2
inst✝⁴ : MulOneClass M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
f : hom
hf : ContinuousAt (⇑f) 1
⊢ Tendsto (⇑f) (𝓝 1) (𝓝 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
⊢ 𝓤 α = comap (fun x ↦ x.1⁻¹ * x.2) (𝓝 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
S : Subgroup G
hS : IsDiscrete ↑S
⊢ ∃ U ∈ 𝓝 1, U⁻¹ = U ∧ ∀ g ∈ S, ((fun x ↦ x * g) '' U ∩ U).Nonempty → g = 1

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
H : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousMul M
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H →* M
hf : ContinuousAt (fun x ↦ (f x.1) x.2) (1, 1)
hl : ∀ (x : G), ContinuousAt (⇑(f x)) 1
hr : ∀ (y : H), ContinuousAt (fun x ↦ (f x) y) 1
x✝ : G × H
x : G
y : H
⊢ ContinuousAt (fun x ↦ (f x.1) x.2) (x, y)

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
u v : UniformSpace G
hu : IsUniformGroup G
hv : IsUniformGroup G
h : 𝓝 1 = 𝓝 1
⊢ 𝓤 G = 𝓤 G

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : (𝓝 1).IsCountablyGenerated
⊢ (𝓤 α).IsCountablyGenerated

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
x : G
h : K ∈ 𝓝 x
y : G
⊢ K ∈ 𝓝 ((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
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
⊢ LocallyCompactSpace G

Tactic:
by

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

Goal state before:
pp: G : Type w
α : Type u
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : TopologicalSpace α
inst✝¹ : Zero α
inst✝ : T1Space α
f : G → α
k : Set G
hk : IsCompact k
hf : support f ⊆ k
h'f : Continuous[inst✝⁵, inst✝²] f
⊢ f = 0 ∨ LocallyCompactSpace G

Tactic:
by

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

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
dr : β × β → β := fun xy ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun xy ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun gx ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun b ↦ Equiv.symm (Equiv.mulLeft b)
⊢ conj ∘ ⇑φ = dr

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
H : Type u_1
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
⊢ IsInducing ⇑f ↔ 𝓝 1 = comap (⇑f) (𝓝 1)

Tactic:
by

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

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
dr : β × β → β := fun xy ↦ xy.2 * xy.1⁻¹
dl : β × β → β := fun xy ↦ xy.1⁻¹ * xy.2
conj : β × β → β := fun gx ↦ gx.1 * gx.2 * gx.1⁻¹
φ : β × β ≃ β × β := (Equiv.refl β).prodShear fun b ↦ Equiv.symm (Equiv.mulLeft b)
conj_φ : conj ∘ ⇑φ = dr
⊢ snd ∘ ⇑φ = dl

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Monoid

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
l : Filter α
f : α → M
hf : Tendsto f l atTop
n : ℕ
hn : 0 < n
⊢ Tendsto (fun x ↦ f x ^ n) l atTop

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Monoid

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hfg : Tendsto (fun x ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map f l, (fun x1 x2 ↦ x1 ≤ x2) x C
x✝¹ : α
x✝ : (fun x1 x2 ↦ x1 ≤ x2) (f x✝¹) C
⊢ (fun x ↦ f x * g x) x✝¹ ≤ (fun x ↦ C * g x) x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Monoid

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l f
hfg : Tendsto (fun x ↦ f x * g x) l atTop
⊢ Tendsto g l atTop

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Monoid

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
h : Tendsto (fun x ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map g l, (fun x1 x2 ↦ x1 ≤ x2) x C
x✝¹ : α
x✝ : (fun x1 x2 ↦ x1 ≤ x2) (g x✝¹) C
⊢ (fun x ↦ f x * g x) x✝¹ ≤ (fun x ↦ f x * C) x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Monoid

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hg : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l g
h : Tendsto (fun x ↦ f x * g x) l atTop
⊢ Tendsto f l atTop

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
H : Type u_1
inst✝⁴ : Monoid H
inst✝³ : TopologicalSpace H
inst✝² : ContinuousConstSMul H H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : 𝓝 1 ≤ map (⇑f) (𝓝 1)
x : G
⊢ map (fun x_1 ↦ f x * x_1) (𝓝 1) = 𝓝 (f 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
H : Type u_1
inst✝⁴ : Monoid H
inst✝³ : TopologicalSpace H
inst✝² : ContinuousConstSMul H H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
⊢ IsOpenMap ⇑f ↔ 𝓝 1 ≤ map (⇑f) (𝓝 1)

Tactic:
by

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

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
⊢ comap (fun gx ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1) = comap snd (𝓝 1)

Tactic:
by

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

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
⊢ Tendsto (fun gx ↦ gx.1 * gx.2 * gx.1⁻¹) (comap snd (𝓝 1)) (𝓝 1)

Tactic:
by

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

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
ι : Type u_3
l : Filter ι
x : ι → β
hx : Tendsto x l (𝓝 1)
g : ι → β
⊢ Tendsto (fun i ↦ (g i, x i)) l (comap Prod.snd (𝓝 1))

Tactic:
by

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

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
ι : Type u_3
l : Filter ι
x : ι → β
hx : Tendsto x l (𝓝 1)
g : ι → β
⊢ Tendsto (g * x * g⁻¹) l (𝓝 1)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
this : ⇑φ ⁻¹' ⇑φ '' U = ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U
k : A
x✝ : k ∈ ↑(↑φ).ker
⊢ Continuous[inst✝⁵, inst✝⁵] fun x ↦ x * k

Tactic:
by

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

Goal state before:
pp: A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
this : ⇑φ ⁻¹' ⇑φ '' U = ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U
⊢ IsOpen[inst✝⁵] (⇑φ ⁻¹' ⇑φ '' U)

Tactic:
by

Goal state after: