mathlib-initiative/mathlib-tactics huggingface dataset:
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✝²] (⋃ a ∈ t, (fun x ↦ x / a) '' s)

Tactic:
]

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
hs : IsOpen[inst✝²] s
⊢ IsOpen[inst✝²] (⋃ a ∈ t, (fun x ↦ x / a) '' s)
Module: Mathlib.Topology.Algebra.Group.Basic

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

Tactic:
]

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
a : G
ha : a ∈ s
b : G
hb : ∀ (o : Set G), IsOpen[inst✝²] o → b ∈ o → (o ∩ t).Nonempty
⊢ a * b ∈ s * t

Tactic:
]

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : 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
⊢ a * b ∈ s * t
Module: Mathlib.Topology.Algebra.Group.Basic

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

Tactic:
]

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
⊢ s * t = s * t

Tactic:
]

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✝²] (op '' s • t)

Tactic:
]

Goal state after:
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✝²] (op '' s • t)
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 ((fun x ↦ x⁻¹) '' s)

Tactic:
]

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : InvolutiveInv G
inst✝ : ContinuousInv G
s : Set G
hs : IsCompact s
⊢ IsCompact ((fun x ↦ x⁻¹) '' s)
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
this : IsClosed[inst✝²] (K * closure[inst✝²] {1})
⊢ K ⊆ K * closure[inst✝²] {1}

Tactic:
]

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
this : IsClosed[inst✝²] (K * closure[inst✝²] {1})
⊢ K ⊆ K * closure[inst✝²] {1}
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
this : IsClosed[inst✝²] (K * closure[inst✝²] {1})
⊢ closure[inst✝²] K ⊆ K * closure[inst✝²] {1}

Tactic:
rw [IsClosed.closure_subset_iff this]

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
this : IsClosed[inst✝²] (K * closure[inst✝²] {1})
⊢ K ⊆ K * closure[inst✝²] {1}
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 * closure[inst✝²] {1}

Tactic:
]

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:
]

Goal state after:
G : Type w
ι' : Sort u_1
inst✝ : Inv G
ts' : ι' → TopologicalSpace G
h' : ∀ (i : ι'), ContinuousInv G
⊢ ContinuousInv G
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 : (fun x1 x2 ↦ x1 * x2) x g ∉ tᶜ
⊢ x ∈ t * ↑⊥.topologicalClosure

Tactic:
]

Goal state after:
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 : (fun x1 x2 ↦ x1 * x2) x g ∉ tᶜ
⊢ x ∈ t * ↑⊥.topologicalClosure
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:
]

Goal state after:
G : Type w
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G
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ᶜ
this : x ∈ t
⊢ False

Tactic:
]

Goal state after:
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ᶜ
this : x ∈ t
⊢ False
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

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

Tactic:
]

Goal state after:
Gᵣ : Type u_3
inst✝² : UniformSpace Gᵣ
inst✝¹ : Group Gᵣ
inst✝ : IsRightUniformGroup Gᵣ
⊢ comap (fun x ↦ x.swap.2 * x.swap.1⁻¹) (𝓝 1) = comap (fun x ↦ x.1 * x.2⁻¹) (𝓝 1)
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
⊢ x ∈ U * U

Tactic:
]

Goal state after:
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
⊢ x ∈ U * U
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
Gᵣ : Type u_3
inst✝² : UniformSpace Gᵣ
inst✝¹ : Group Gᵣ
inst✝ : IsRightUniformGroup Gᵣ
⊢ comap (fun x ↦ x.swap.2 / x.swap.1) (𝓝 1) = comap (fun x ↦ x.1 / x.2) (𝓝 1)
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
a : G
s : Set G
hs : s ∈ 𝓝 a
this : Tendsto (fun p ↦ p.1 * p.2) (𝓝 (a, 1)) (𝓝 a)
U : Set G
hU : U ∈ 𝓝 a
V : Set G
hV : V ∈ 𝓝 1
hUV : image2 HMul.hMul U V ⊆ s
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst✝²] t ∧ t ⊆ s

Tactic:
]

Goal state after:
G : Type w
H : Type x
α : Type u
β : Type v
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
this : Tendsto (fun p ↦ p.1 * p.2) (𝓝 (a, 1)) (𝓝 a)
U : Set G
hU : U ∈ 𝓝 a
V : Set G
hV : V ∈ 𝓝 1
hUV : image2 HMul.hMul U V ⊆ s
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst✝²] t ∧ t ⊆ s
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 ((Homeomorph.mulRight y⁻¹) x) ((Homeomorph.mulRight y⁻¹) y) ↔ Inseparable (x / y) 1

Tactic:
]

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x y : G
⊢ Inseparable ((Homeomorph.mulRight y⁻¹) x) ((Homeomorph.mulRight y⁻¹) y) ↔ Inseparable (x / y) 1
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

Tactic:
]

Goal state after:
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
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 ∈ 𝓝 1

Tactic:
]

Goal state after:
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 ∈ 𝓝 1
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:
]

Goal state after:
α : 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 (𝓤 α)
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 ∈ map Inv.inv (𝓝 1)
⊢ S⁻¹ ∈ 𝓝 1

Tactic:
]

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Set G
hS : S ∈ map Inv.inv (𝓝 1)
⊢ S⁻¹ ∈ 𝓝 1
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:
]

Goal state after:
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 = ↑⊤
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 g

Tactic:
]

Goal state after:
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 g
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 ∈ (fun x ↦ g * x) '' connectedComponent 1

Tactic:
]

Goal state after:
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 ∈ (fun x ↦ g * x) '' connectedComponent 1
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:
]

Goal state after:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : DivisionMonoid G
inst✝ : ContinuousInv G
g : G
hg : g ∈ connectedComponent 1
⊢ g⁻¹ ∈ connectedComponent 1⁻¹
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
⊢ Tendsto id 𝓕 (𝓤 α) ↔ Tendsto ((Prod.mk 1 ∘ fun x ↦ x.2 * x.1⁻¹) * fun x ↦ (x.1, x.1)) 𝓕 (𝓤 α)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
⊢ Tendsto id 𝓕 (𝓤 α) ↔ Tendsto ((Prod.mk 1 ∘ fun x ↦ x.2 * x.1⁻¹) * fun x ↦ (x.1, x.1)) 𝓕 (𝓤 α)
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
⊢ g ∈ U * U

Tactic:
]

Goal state after:
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
⊢ g ∈ U * U
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
⊢ (Filter.comap (fun x_1 ↦ x_1 * x⁻¹) (𝓝 1)).HasBasis p fun i ↦ {y | y / x ∈ s i}

Tactic:
]

Goal state after:
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
⊢ (Filter.comap (fun x_1 ↦ x_1 * x⁻¹) (𝓝 1)).HasBasis p fun i ↦ {y | y / x ∈ s i}
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
⊢ (∀ i ∈ 𝓝 1, ∃ y ∈ s, y ∈ {y | y / x ∈ id i}) ↔ ∀ U ∈ 𝓝 1, ∃ y ∈ s, y / x ∈ U

Tactic:
]

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x : G
s : Set G
⊢ (∀ i ∈ 𝓝 1, ∃ y ∈ s, y ∈ {y | y / x ∈ id i}) ↔ ∀ U ∈ 𝓝 1, ∃ y ∈ s, y / x ∈ U
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
⊢ Tendsto id 𝓕 (𝓤 α) ↔ Tendsto ((fun x ↦ (x.1, x.1)) * Prod.mk 1 ∘ fun x ↦ x.1⁻¹ * x.2) 𝓕 (𝓤 α)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
𝓕 : Filter (α × α)
⊢ Tendsto id 𝓕 (𝓤 α) ↔ Tendsto ((fun x ↦ (x.1, x.1)) * Prod.mk 1 ∘ fun x ↦ x.1⁻¹ * x.2) 𝓕 (𝓤 α)
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 : Set G
hU : U ∈ 𝓝 1
hUinv : U⁻¹ = U
h : ∀ g ∈ S, ((fun x ↦ g * x) '' U ∩ U).Nonempty → g = 1
g : G
hgS : g ∈ S
hgU : ((fun x ↦ x * g) '' U ∩ U).Nonempty
⊢ ((fun x ↦ x * g) '' U ∩ U).Nonempty

Tactic:
]

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete ↑S
U : Set G
hU : U ∈ 𝓝 1
hUinv : U⁻¹ = U
h : ∀ g ∈ S, ((fun x ↦ g * x) '' U ∩ U).Nonempty → g = 1
g : G
hgS : g ∈ S
hgU : ((fun x ↦ x * g) '' U ∩ U).Nonempty
⊢ ((fun x ↦ x * g) '' U ∩ U).Nonempty
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
⊢ (∀ (x : G), 𝓝 x = comap (⇑f) (𝓝 (f x))) ↔ 𝓝 1 = comap (⇑f) (𝓝 1)

Tactic:
]

Goal state after:
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
⊢ (∀ (x : G), 𝓝 x = comap (⇑f) (𝓝 (f x))) ↔ 𝓝 1 = comap (⇑f) (𝓝 1)
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
⊢ comap (fun x ↦ x.2 / x.1) (𝓝 1) = comap (fun x ↦ x.2 / x.1) (𝓝 1)

Tactic:
]

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
⊢ (comap (fun x ↦ x.2 / x.1) (𝓝 1)).IsCountablyGenerated

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : (𝓝 1).IsCountablyGenerated
⊢ (comap (fun x ↦ x.2 / x.1) (𝓝 1)).IsCountablyGenerated
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: case refine_2
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
⊢ (fun x_1 ↦ (y * x⁻¹)⁻¹ • x_1) ⁻¹' K ∈ 𝓝 y

Tactic:
]

Goal state after:
case refine_2
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
⊢ (fun x_1 ↦ (y * x⁻¹)⁻¹ • x_1) ⁻¹' K ∈ 𝓝 y
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
hf : 𝓝 1 = comap (⇑f) (𝓝 1)
x : G
⊢ comap (⇑f ∘ fun x_1 ↦ x_1 * x⁻¹) (𝓝 1) = comap ((fun x_1 ↦ x_1 * (f x)⁻¹) ∘ ⇑f) (𝓝 1)

Tactic:
]

Goal state after:
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
hf : 𝓝 1 = comap (⇑f) (𝓝 1)
x : G
⊢ comap (⇑f ∘ fun x_1 ↦ x_1 * x⁻¹) (𝓝 1) = comap ((fun x_1 ↦ x_1 * (f x)⁻¹) ∘ ⇑f) (𝓝 1)
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
this : map (fun x_1 ↦ f x * x_1) (𝓝 1) = 𝓝 (f x)
⊢ map (fun x_1 ↦ f x * x_1) (𝓝 1) ≤ map (fun x_1 ↦ f (x * x_1)) (𝓝 1)

Tactic:
]

Goal state after:
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
this : map (fun x_1 ↦ f x * x_1) (𝓝 1) = 𝓝 (f x)
⊢ map (fun x_1 ↦ f x * x_1) (𝓝 1) ≤ map (fun x_1 ↦ f (x * x_1)) (𝓝 1)
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_φ : snd ∘ ⇑φ = dl
⊢ 𝓤 β = 𝓤 β

Tactic:
]

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 snd (𝓝 1) ≤ comap snd (𝓝 1)

Tactic:
]

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
⊢ IsOpen[inst✝⁵] (⇑φ ⁻¹' ⇑φ '' U)

Tactic:
]

Goal state after:
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
⊢ IsOpen[inst✝⁵] (⇑φ ⁻¹' ⇑φ '' U)
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 (Prod.snd ∘ fun i ↦ (g i, x i)) l (𝓝 1)

Tactic:
]

Goal state after:
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
ι : Type u_3
l : Filter ι
x : ι → β
hx : Tendsto x l (𝓝 1)
g : ι → β
⊢ Tendsto (Prod.snd ∘ fun i ↦ (g i, x i)) l (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case right
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
x k : A
hk : φ k = 1
hx : x ∈ (fun h ↦ (fun x ↦ x * k) ⁻¹' U) hk
⊢ φ x = φ x

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
t t' : TopologicalSpace G
tg : IsTopologicalGroup G
tg' : IsTopologicalGroup G
h : 𝓝 1 = 𝓝 1
x : G
⊢ comap (fun x_1 ↦ x_1 * x⁻¹) (𝓝 1) = comap (fun x_1 ↦ x_1 * x⁻¹) (𝓝 1)

Tactic:
]

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

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
this : Tendsto φ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
⊢ Tendsto (((fun x ↦ x.2 * x.1⁻¹) ∘ fun x ↦ (x.1.1 / x.1.2, x.2.1 / x.2.2)) ∘ fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
    (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

Tactic:
]

Goal state after:
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
this : Tendsto φ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
⊢ Tendsto (((fun x ↦ x.2 * x.1⁻¹) ∘ fun x ↦ (x.1.1 / x.1.2, x.2.1 / x.2.2)) ∘ fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
    (𝓤 β ×ˢ 𝓤 β) (𝓝 1)