mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun x ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i ↦ S.restrictPreimage (φ i)
S : Set α
hS : S ∈ 𝔖
I : Set ι
I_finite : I.Finite
I_cover : S ⊆ ⋃ i ∈ I, range (φ i)
⊢ ⋃ i ∈ I, range (ψ S i) = univ

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun x ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i ↦ S.restrictPreimage (φ i)
S : Set α
hS : S ∈ 𝔖
I : Set ι
I_finite : I.Finite
I_cover : S ⊆ ⋃ i ∈ I, range (φ i)
⊢ S ⊆ ⋃ i ∈ I, range (φ i)
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SMul M α
inst✝³ : ContinuousConstSMul M α
inst✝² : TopologicalSpace β
g : β → α
b : β
s : Set β
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
c : M
⊢ Continuous[inst✝⁵, inst✝⁵] fun x ↦ MulOpposite.op c • x

Tactic:
simpa using

Goal state after:
M : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SMul M α
inst✝³ : ContinuousConstSMul M α
inst✝² : TopologicalSpace β
g : β → α
b : β
s : Set β
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
c : M
⊢ Continuous[inst✝⁵, inst✝⁵] fun x ↦ c • x
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : SMul M α
inst✝² : ContinuousConstSMul M α
N : Type u_4
β : Type u_5
inst✝¹ : SMul N β
inst✝ : TopologicalSpace β
g : β → α
hg : IsInducing g
f : N → M
hf : ∀ {c : N} {x : β}, g (c • x) = f c • g x
c : N
⊢ Continuous[inst✝, inst✝] fun x ↦ c • x

Tactic:
simpa using

Goal state after:
M : Type u_1
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : SMul M α
inst✝² : ContinuousConstSMul M α
N : Type u_4
β : Type u_5
inst✝¹ : SMul N β
inst✝ : TopologicalSpace β
g : β → α
hg : IsInducing g
f : N → M
hf : ∀ {c : N} {x : β}, g (c • x) = f c • g x
c : N
⊢ Continuous[inst✝, inst✝⁴] fun x ↦ f c • g x
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: α : Type u_2
β : Type u_3
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
f : β → α
l : Filter β
a : α
c : G
h : Tendsto (fun x ↦ c • f x) l (𝓝 (c • a))
⊢ Tendsto f l (𝓝 a)

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
f : β → α
l : Filter β
a : α
c : G
h : Tendsto (fun x ↦ c • f x) l (𝓝 (c • a))
⊢ Tendsto f l (𝓝 a)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
t : Set α
hF : ∀ᶠ (i : ι) in p, ∀ x ∈ t, F i x ∈ s
hf : ∀ x ∈ t, f x ∈ s
g : β → γ
hg : UniformContinuousOn g s
h : TendstoUniformlyOn F f p t
⊢ ∀ᶠ (i : ι) in p, ∀ (x : ↑t), t.domRestrict (F i) x ∈ s

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
t : Set α
hF : ∀ᶠ (i : ι) in p, ∀ x ∈ t, F i x ∈ s
hf : ∀ x ∈ t, f x ∈ s
g : β → γ
hg : UniformContinuousOn g s
h : TendstoUniformlyOn F f p t
⊢ ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a ∈ s
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
t : Set α
hF : ∀ᶠ (i : ι) in p, ∀ x ∈ t, F i x ∈ s
hf : ∀ x ∈ t, f x ∈ s
g : β → γ
hg : UniformContinuousOn g s
h : TendstoUniformlyOn F f p t
⊢ ∀ (x : ↑t), t.domRestrict f x ∈ s

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
t : Set α
hF : ∀ᶠ (i : ι) in p, ∀ x ∈ t, F i x ∈ s
hf : ∀ x ∈ t, f x ∈ s
g : β → γ
hg : UniformContinuousOn g s
h : TendstoUniformlyOn F f p t
⊢ ∀ a ∈ t, f a ∈ s
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: α : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
x : α
inst✝ : IsPretransitive G α
hx : IsClosed[inst✝⁴] {x}
g : G
⊢ IsClosed[inst✝⁴] {g • x}

Tactic:
rw [← image_singleton, image_smul]

Goal state after:
α : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
x : α
inst✝ : IsPretransitive G α
hx : IsClosed[inst✝⁴] {x}
g : G
⊢ IsClosed[inst✝⁴] (g • {x})
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: α : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
x : α
inst✝ : IsPretransitive G α
hx : IsOpen[inst✝⁴] {x}
g : G
⊢ IsOpen[inst✝⁴] {g • x}

Tactic:
rw [← image_singleton, image_smul]

Goal state after:
α : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
x : α
inst✝ : IsPretransitive G α
hx : IsOpen[inst✝⁴] {x}
g : G
⊢ IsOpen[inst✝⁴] (g • {x})
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_6
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
a b : M
h : a ⤳ b
n x✝ : ℕ
ihn : (a ^ x✝) ⤳ (b ^ x✝)
⊢ (a ^ x✝.succ) ⤳ (b ^ x✝.succ)

Tactic:
simpa using

Goal state after:
M : Type u_6
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
a b : M
h : a ⤳ b
n x✝ : ℕ
ihn : (a ^ x✝) ⤳ (b ^ x✝)
⊢ (a ^ x✝ * a) ⤳ (b ^ x✝ * b)
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Mul M
inst✝⁵ : ContinuousMul M
inst✝⁴ : TopologicalSpace N
inst✝³ : Monoid N
inst✝² : ContinuousMul N
inst✝¹ : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst✝ : l.NeBot
h₁ : Tendsto (fun x ↦ ↑(f x)) l (𝓝 r₁)
h₂ : Tendsto (fun x ↦ ↑(f x)⁻¹) l (𝓝 r₂)
⊢ 1 = r₁ * r₂

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Mul M
inst✝⁵ : ContinuousMul M
inst✝⁴ : TopologicalSpace N
inst✝³ : Monoid N
inst✝² : ContinuousMul N
inst✝¹ : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst✝ : l.NeBot
h₁ : Tendsto (fun x ↦ ↑(f x)) l (𝓝 r₁)
h₂ : Tendsto (fun x ↦ ↑(f x)⁻¹) l (𝓝 r₂)
⊢ 1 = r₁ * r₂
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Mul M
inst✝⁵ : ContinuousMul M
inst✝⁴ : TopologicalSpace N
inst✝³ : Monoid N
inst✝² : ContinuousMul N
inst✝¹ : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst✝ : l.NeBot
h₁ : Tendsto (fun x ↦ ↑(f x)) l (𝓝 r₁)
h₂ : Tendsto (fun x ↦ ↑(f x)⁻¹) l (𝓝 r₂)
⊢ 1 = r₂ * r₁

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Mul M
inst✝⁵ : ContinuousMul M
inst✝⁴ : TopologicalSpace N
inst✝³ : Monoid N
inst✝² : ContinuousMul N
inst✝¹ : T2Space N
f : ι → Nˣ
r₁ r₂ : N
l : Filter ι
inst✝ : l.NeBot
h₁ : Tendsto (fun x ↦ ↑(f x)) l (𝓝 r₁)
h₂ : Tendsto (fun x ↦ ↑(f x)⁻¹) l (𝓝 r₂)
⊢ 1 = r₂ * r₁
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
s t V : Set M
V_in : V ∈ 𝓝 0
hV' : s * V ⊆ U
W : Set M
W_in : W ∈ 𝓝 0
hW' : t * W ⊆ U
⊢ (s ∪ t) * (V ∩ W) ⊆ U

Tactic:
rw [union_mul]

Goal state after:
case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
s t V : Set M
V_in : V ∈ 𝓝 0
hV' : s * V ⊆ U
W : Set M
W_in : W ∈ 𝓝 0
hW' : t * W ⊆ U
⊢ s * (V ∩ W) ∪ t * (V ∩ W) ⊆ U
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
hx : x ∈ K
⊢ U ∈ 𝓝 (x * 0)

Tactic:
simpa using

Goal state after:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
x : M
hx : x ∈ K
⊢ U ∈ 𝓝 0
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
h'l : l ≤ (𝓝 0).coprod (𝓝 0)
⊢ Tendsto (fun x ↦ x.1 * x.2) l (𝓝 0)

Tactic:
simpa using

Goal state after:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
h'l : l ≤ (𝓝 0).coprod (𝓝 0)
⊢ Tendsto (fun x ↦ x.1 * x.2) l (𝓝 0)
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen[inst✝³] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
x : M
hx : x ≠ 0
hxW : x ∈ W
⊢ 1 ∈ univ * W

Tactic:
simpa using

Goal state after:
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen[inst✝³] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
x : M
hx : x ≠ 0
hxW : x ∈ W
⊢ 1 ∈ univ * W
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen[inst✝³] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
H : ¬∃ x, x ≠ 0 ∧ x ∈ W
⊢ W ⊆ {0}

Tactic:
simpa using

Goal state after:
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen[inst✝³] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
H : ¬∃ x, x ≠ 0 ∧ x ∈ W
⊢ ∀ y ∈ W, y = 0
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen[inst✝³] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
H : ¬∃ x, x ≠ 0 ∧ x ∈ W
⊢ {0} ⊆ W

Tactic:
simpa using

Goal state after:
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen[inst✝³] U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
H : ¬∃ x, x ≠ 0 ∧ x ∈ W
⊢ 0 ∈ W
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulOneClass M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
⊢ ∃ V, IsOpen[inst✝²] V ∧ 1 ∈ V ∧ V * V ⊆ U

Tactic:
simpa using

Goal state after:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulOneClass M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
⊢ ∃ V, IsOpen[inst✝²] V ∧ 1 ∈ V ∧ ∀ x ∈ V, ∀ y ∈ V, x * y ∈ U
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W
v w s t : M
v_in : v ∈ V
w_in : w ∈ V
s_in : s ∈ V
t_in : t ∈ V
⊢ v * w * s * t ∈ u

Tactic:
simpa using

Goal state after:
case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W
v w s t : M
v_in : v ∈ V
w_in : w ∈ V
s_in : s ∈ V
t_in : t ∈ V
⊢ v * (w * (s * t)) ∈ u
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
⊢ Continuous[inst✝², inst✝²] fun a ↦ a ^ 0

Tactic:
simpa using

Goal state after:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
⊢ Continuous[inst✝², inst✝²] fun a ↦ 1
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case mk
ι : Type u_1
α : Type u_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
l : List ι
⊢ (∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, Tendsto (f i) x (𝓝 (a i))) →
    Tendsto (fun b ↦ (Multiset.map (fun c ↦ f c b) (Quot.mk (⇑(List.isSetoid ι)) l)).prod) x
      (𝓝 (Multiset.map a (Quot.mk (⇑(List.isSetoid ι)) l)).prod)

Tactic:
simpa using

Goal state after:
case mk
ι : Type u_1
α : Type u_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
l : List ι
⊢ (∀ i ∈ l, Tendsto (f i) x (𝓝 (a i))) → Tendsto (fun b ↦ (List.map (fun c ↦ f c b) l).prod) x (𝓝 (List.map a l).prod)
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case mk
ι : 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
s : Multiset ι
l : List ι
⊢ (∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, Continuous[inst✝³, inst✝²] (f i)) →
    Continuous[inst✝³, inst✝²] fun a ↦ (Multiset.map (fun i ↦ f i a) (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Tactic:
simpa using

Goal state after:
case mk
ι : 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
s : Multiset ι
l : List ι
⊢ (∀ i ∈ l, Continuous[inst✝³, inst✝²] (f i)) → Continuous[inst✝³, inst✝²] fun a ↦ (List.map (fun i ↦ f i a) l).prod
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case mk
ι : 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
s : Multiset ι
t : Set X
l : List ι
⊢ (∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, ContinuousOn (f i) t) →
    ContinuousOn (fun a ↦ (Multiset.map (fun i ↦ f i a) (Quot.mk (⇑(List.isSetoid ι)) l)).prod) t

Tactic:
simpa using

Goal state after:
case mk
ι : 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
s : Multiset ι
t : Set X
l : List ι
⊢ (∀ i ∈ l, ContinuousOn (f i) t) → ContinuousOn (fun a ↦ (List.map (fun i ↦ f i a) l).prod) t
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : MapClusterPt y ℱ f
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ

Tactic:
rw [H.2.1.mapClusterPt_iff_lift'_closure H.1] at hy

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure[inst✝¹] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ
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:
simpa using

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

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul α α
s : Set α
a : α
h : s ∈ 𝓝 1
⊢ {a} * s ∈ 𝓝 a
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:
simpa using

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s : Set α
a : α
h : s ∈ 𝓝 1
⊢ s * {a} ∈ 𝓝 a
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:
simpa using

Goal state after:
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
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'
b : G
hb : b ∈ s
hc : (fun x ↦ x * y) b ∈ s'
⊢ y ∈ s * s'

Tactic:
simpa using

Goal state after:
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'
b : G
hb : b ∈ s
hc : (fun x ↦ x * y) b ∈ s'
⊢ y ∈ s * s'
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:
simpa using

Goal state after:
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
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
b : G
hb : b ∈ s'
hc : (fun x ↦ y * x) b ∈ s
⊢ y ∈ s * s'

Tactic:
simpa using

Goal state after:
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
b : G
hb : b ∈ s'
hc : (fun x ↦ y * x) b ∈ s
⊢ y ∈ s * s'
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:
simpa using

Goal state after:
G : Type u_1
inst✝³ : DivInvMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
inst✝ : ContinuousInv G
x y : G
h : x ⤳ y
n : ℕ
⊢ (x ^ n) ⤳ (y ^ n)
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:
simpa using

Goal state after:
G : Type u_1
inst✝³ : DivInvMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
inst✝ : ContinuousInv G
x y : G
h : x ⤳ y
n : ℕ
⊢ (x ^ (n + 1))⁻¹ ⤳ (y ^ (n + 1))⁻¹
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:
simpa using

Goal state after:
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)
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 rw [hF.closure_eq]

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
⊢ x ∈ t * ↑⊥.topologicalClosure

Tactic:
exact ⟨x * g, H, g⁻¹, Subgroup.inv_mem _ hg, by simp⟩

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:
simpa using

Goal state after:
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✝¹] fun x ↦ (f x)⁻¹
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

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

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
n : ℕ
⊢ Continuous[inst✝², inst✝²] fun a ↦ a ^ n
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:
simpa using

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
n : ℕ
⊢ Continuous[inst✝², inst✝²] fun a ↦ (a ^ (n + 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 Prod.swap (𝓤 Gᵣ) = comap (fun x ↦ x.1 / x.2) (𝓝 1)

Tactic:
uniformity_eq_comap_nhds_one,

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