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

Goal state before:
pp: case empty
α : Type u_3
β : Type u_4
ι : Type u_5
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : ι → β → α
h : ∀ i ∈ ∅, UniformContinuous (f i)
⊢ UniformContinuous fun x ↦ ∏ i ∈ ∅, f i x

Tactic:
simpa using

Goal state after:
case empty
α : Type u_3
β : Type u_4
ι : Type u_5
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : ι → β → α
h : ∀ i ∈ ∅, UniformContinuous (f i)
⊢ UniformContinuous fun x ↦ 1
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:
simpa using

Goal state after:
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)
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:
simpa using

Goal state after:
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)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: case cons
α : Type u_3
β : Type u_4
ι : Type u_5
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : ι → β → α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, UniformContinuous (f i)) → UniformContinuous fun x ↦ ∏ i ∈ s, f i x
h : UniformContinuous (f a) ∧ ∀ a ∈ s, UniformContinuous (f a)
⊢ UniformContinuous fun x ↦ ∏ i ∈ cons a s ha, f i x

Tactic:
simpa using

Goal state after:
case cons
α : Type u_3
β : Type u_4
ι : Type u_5
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : ι → β → α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, UniformContinuous (f i)) → UniformContinuous fun x ↦ ∏ i ∈ s, f i x
h : UniformContinuous (f a) ∧ ∀ a ∈ s, UniformContinuous (f a)
⊢ UniformContinuous fun x ↦ f a x * ∏ i ∈ s, f i x
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:
simpa using

Goal state after:
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)
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:
simpa using

Goal state after:
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)
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:
simpa using

Goal state after:
α : 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 (𝓤 α)
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:
simpa using

Goal state after:
α : 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 (𝓤 α)
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:
simpa using

Goal state after:
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
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
hmul : g ∈ connectedComponent (g * h)
⊢ g * h ∈ connectedComponent g

Tactic:
simpa using

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
hmul : g ∈ connectedComponent (g * h)
⊢ g * h ∈ connectedComponent (g * h)
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
this : (fun p ↦ p.1 * p.2⁻¹) ⁻¹' s ∈ 𝓝 (1, 1)
⊢ ∃ V ∈ 𝓝 1, ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s

Tactic:
simpa using

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : s ∈ 𝓝 1
this : (fun p ↦ p.1 * p.2⁻¹) ⁻¹' s ∈ 𝓝 (1, 1)
⊢ ∃ V ∈ 𝓝 1, ∀ v ∈ V, ∀ w ∈ V, v * w⁻¹ ∈ s
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:
simpa using

Goal state after:
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
⊢ Tendsto (fun x_1 ↦ f x * f x_1) (𝓝 1) (𝓝 (f x))
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:
simpa using

Goal state after:
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)
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:
simpa using

Goal state after:
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 ∈ 𝓝 x
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
x : α
hx : 1 ≤ f x
⊢ f x ≤ (fun x ↦ f x ^ n) x

Tactic:
simpa using

Goal state after:
α : 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
x : α
hx : 1 ≤ f x
⊢ f x ≤ f x ^ n
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:
obtain ⟨C, hC⟩ := hg

Goal state after:
α : 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
⊢ Tendsto f l atTop
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hinv : Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
x₀ : G
this : Tendsto (fun x ↦ x₀⁻¹ * (x₀ * x⁻¹ * x₀⁻¹)) (𝓝 1) (map (fun x ↦ x₀⁻¹ * x) (𝓝 1))
⊢ ContinuousAt (fun a ↦ a⁻¹) x₀

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hinv : Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
x₀ : G
this : Tendsto (fun x ↦ x₀⁻¹ * (x₀ * x⁻¹ * x₀⁻¹)) (𝓝 1) (map (fun x ↦ x₀⁻¹ * x) (𝓝 1))
⊢ Tendsto (fun x ↦ x⁻¹ * x₀⁻¹) (𝓝 1) (map (fun x ↦ x₀⁻¹ * x) (𝓝 1))
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
x₀ : G
hconj : ∀ (x₀ : G), map (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) = 𝓝 1
⊢ 𝓝 x₀ = map (fun x ↦ x * x₀) (map (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1))

Tactic:
simpa using

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
x₀ : G
hconj : ∀ (x₀ : G), map (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) = 𝓝 1
⊢ 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : (𝓝 1).HasBasis (fun x ↦ True) u
u_anti : Antitone u
⊢ Tendsto ?m.78 (𝓝 (1, 1)) (𝓝 1)

Tactic:
simpa using

Goal state after:
G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : FirstCountableTopology G
u : ℕ → Set G
hu : (𝓝 1).HasBasis (fun x ↦ True) u
u_anti : Antitone u
⊢ Tendsto ?m.78 (𝓝 (1, 1)) (𝓝 1)
Module: Mathlib.Order.Filter.AtTopBot.Ring

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atBot
this : Tendsto (fun x ↦ f x * (Neg.neg ∘ g) x) l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atBot

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atBot
this : Tendsto (fun x ↦ f x * (Neg.neg ∘ g) x) l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atBot
Module: Mathlib.Order.Filter.AtTopBot.Ring

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atTop
this : Tendsto (fun x ↦ -f x * g x) l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atBot

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atTop
this : Tendsto (fun x ↦ -f x * g x) l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atBot
Module: Mathlib.Order.Filter.AtTopBot.Ring

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atBot
this : Tendsto (fun x ↦ -f x * -g x) l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atTop

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atBot
this : Tendsto (fun x ↦ -f x * -g x) l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atTop
Module: Mathlib.Order.Filter.AtTopBot.Ring

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ ¬Tendsto (fun x ↦ x ^ 0) atTop atBot

Tactic:
by simp [not_tendsto_const_atBot]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto (fun x ↦ f x * r) l atTop ↔ Tendsto f l atTop

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto (fun x ↦ r * f x) l atTop ↔ Tendsto f l atTop
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto (fun x ↦ f x / r) l atTop ↔ Tendsto f l atTop

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto (fun x ↦ f x * r⁻¹) l atTop ↔ Tendsto f l atTop
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x / r) l atTop

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x * r⁻¹) l atTop
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
α : Type u_1
l : Filter α
x : G
u : α → G
A : Tendsto (fun x_1 ↦ x) l (𝓝 x)
h : Tendsto (fun x_1 ↦ u x_1 / x) l (𝓝 1)
⊢ Tendsto u l (𝓝 x)

Tactic:
simpa using

Goal state after:
G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
α : Type u_1
l : Filter α
x : G
u : α → G
A : Tendsto (fun x_1 ↦ x) l (𝓝 x)
h : Tendsto (fun x_1 ↦ u x_1 / x) l (𝓝 1)
⊢ Tendsto u l (𝓝 x)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
α : Type u_1
l : Filter α
x : G
u : α → G
A : Tendsto (fun x_1 ↦ x) l (𝓝 x)
h : Tendsto u l (𝓝 x)
⊢ Tendsto (fun x_1 ↦ u x_1 / x) l (𝓝 1)

Tactic:
simpa using

Goal state after:
G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
α : Type u_1
l : Filter α
x : G
u : α → G
A : Tendsto (fun x_1 ↦ x) l (𝓝 x)
h : Tendsto u l (𝓝 x)
⊢ Tendsto (fun x_1 ↦ u x_1 / x) l (𝓝 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
p : α → Prop
hp : ∀ᶠ (x : α) in 𝓝 1, p x
⊢ ∀ᶠ (x : α) in 𝓝 1, ∀ (g : α), p (g * x * g⁻¹)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
p : α → Prop
hp : ∀ᶠ (x : α) in 𝓝 1, p x
⊢ ∀ᶠ (x : α) in 𝓝 1, ∀ (g : α), p (g * x * g⁻¹)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
α : Type u_1
l : Filter α
inst✝¹ : l.NeBot
inst✝ : T2Space G
f g : α → G
a b : G
hf : Tendsto f l (𝓝 a)
hg : Tendsto g l (𝓝 b)
hfg : Tendsto (fun x ↦ f x / g x) l (𝓝 1)
⊢ Tendsto f l (𝓝 b)

Tactic:
simpa using

Goal state after:
G : Type w
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
α : Type u_1
l : Filter α
inst✝¹ : l.NeBot
inst✝ : T2Space G
f g : α → G
a b : G
hf : Tendsto f l (𝓝 a)
hg : Tendsto g l (𝓝 b)
hfg : Tendsto (fun x ↦ f x / g x) l (𝓝 1)
⊢ Tendsto f l (𝓝 b)
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto (fun x ↦ r * f x) l atBot ↔ Tendsto f l atBot

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto (fun x ↦ r * -f x) l atTop ↔ Tendsto (fun x ↦ -f x) l atTop
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
α : Type u_1
l : Filter α
inst✝¹ : l.NeBot
inst✝ : T2Space G
f g : α → G
a : G
hf : Tendsto f l (𝓝 a)
hg : Tendsto g l (𝓝 a)
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 1)

Tactic:
simpa using

Goal state after:
G : Type w
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
α : Type u_1
l : Filter α
inst✝¹ : l.NeBot
inst✝ : T2Space G
f g : α → G
a : G
hf : Tendsto f l (𝓝 a)
hg : Tendsto g l (𝓝 a)
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 1)
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto (fun x ↦ f x * r) l atBot ↔ Tendsto f l atBot

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto (fun x ↦ r * f x) l atBot ↔ Tendsto f l atBot
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x : G
⊢ comap (fun x_1 ↦ x_1 / x) (𝓝 1) = 𝓝 x

Tactic:
simpa using

Goal state after:
G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x : G
⊢ comap (fun x_1 ↦ x_1 * x⁻¹) (𝓝 1) = 𝓝 x
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x ↦ r * f x) l atTop ↔ Tendsto f l atBot

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x ↦ r * f x) l atTop ↔ Tendsto f l atBot
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x ↦ f x * r) l atTop ↔ Tendsto f l atBot

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x ↦ r * f x) l atTop ↔ Tendsto f l atBot
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x ↦ r * f x) l atBot ↔ Tendsto f l atTop

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x ↦ r * f x) l atBot ↔ Tendsto f l atTop
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x ↦ f x * r) l atBot ↔ Tendsto f l atTop

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x ↦ r * f x) l atBot ↔ Tendsto f l atTop
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsClosed[inst✝²] {1}
x : G
⊢ IsClosed[inst✝²] {x}

Tactic:
simpa using

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
h : IsClosed[inst✝²] {1}
x : G
⊢ IsClosed[inst✝²] {x}
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : IsUniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
hf : ContinuousAt (⇑f) 1
⊢ Tendsto (⇑f) (𝓝 1) (𝓝 1)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : IsUniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
hf : ContinuousAt (⇑f) 1
⊢ Tendsto (⇑f) (𝓝 1) (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case right
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
s t V : Set G
V_in : V ∈ 𝓝 1
hV' : s * V ⊆ U
W : Set G
W_in : W ∈ 𝓝 1
hW' : t * W ⊆ U
⊢ (s ∪ t) * (V ∩ W) ⊆ U

Tactic:
rw [union_mul]

Goal state after:
case right
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
s t V : Set G
V_in : V ∈ 𝓝 1
hV' : s * V ⊆ U
W : Set G
W_in : W ∈ 𝓝 1
hW' : t * W ⊆ U
⊢ s * (V ∩ W) ∪ t * (V ∩ W) ⊆ U
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
x : G
hx : x ∈ K
⊢ U ∈ 𝓝 (x * 1)

Tactic:
simpa using

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
x : G
hx : x ∈ K
⊢ U ∈ 𝓝 x
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
U : Set G
H : U ∈ 𝓝 1
V : Set G
V_nhds : V ∈ 𝓝 1
V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U
x y z : G
hz₁ : (x, z) ∈ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V
hz₂ : (z, y) ∈ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V
⊢ (x, y) ∈ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' U

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
U : Set G
H : U ∈ 𝓝 1
V : Set G
V_nhds : V ∈ 𝓝 1
V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U
x y z : G
hz₁ : (x, z) ∈ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V
hz₂ : (z, y) ∈ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V
⊢ y * x⁻¹ ∈ U