mathlib-initiative/mathlib-tactics huggingface dataset:
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 α
s : Set G
t : Set α
ht : IsOpen[inst✝³] t
⊢ IsOpen[inst✝³] (⋃ a ∈ s, a • t)

Tactic:
]

Goal state after:
α : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
s : Set G
t : Set α
ht : IsOpen[inst✝³] t
⊢ IsOpen[inst✝³] (⋃ a ∈ s, a • t)
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
⊢ TendstoUniformly (fun n ↦ t.domRestrict fun x ↦ g (F n x)) (t.domRestrict fun x ↦ g (f x)) p

Tactic:
]

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
⊢ TendstoUniformly (fun n ↦ t.domRestrict fun x ↦ g (F n x)) (t.domRestrict fun x ↦ g (f x)) p
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: G : Type u_4
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousConstSMul G G
g : G
s : Set G
⊢ g⁻¹ • g • s ∈ 𝓝 (g⁻¹ • g) ↔ s ∈ 𝓝 1

Tactic:
]

Goal state after:
G : Type u_4
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousConstSMul G G
g : G
s : Set G
⊢ g⁻¹ • g • s ∈ 𝓝 (g⁻¹ • g) ↔ s ∈ 𝓝 1
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:
]

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 α
⊢ (∀ (a : α), IsOpen[inst✝⁴] {a}) ↔ IsOpen[inst✝⁴] {x}

Tactic:
]

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 α
⊢ (∀ (a : α), IsOpen[inst✝⁴] {a}) ↔ IsOpen[inst✝⁴] {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:
]

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.ConstMulAction

Goal state before:
pp: case inl.inr
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
hs : s.Nonempty
⊢ closure[inst✝²] 0 = 0

Tactic:
]

Goal state after:
case inl.inr
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
hs : s.Nonempty
⊢ closure[inst✝²] 0 = 0
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: α : Type u_2
inst✝⁶ : TopologicalSpace α
M : Type u_4
β : Type u_5
inst✝⁵ : Semiring M
inst✝⁴ : AddCommMonoid α
inst✝³ : Module M α
inst✝² : ContinuousConstSMul M α
inst✝¹ : AddMonoid β
f : α →+ β
inst✝ : TopologicalSpace β
hf : IsQuotientMap ⇑f
n : ℕ
hc : IsUnit ↑n
⊢ IsUnit ↑n

Tactic:
]

Goal state after:
α : Type u_2
inst✝⁶ : TopologicalSpace α
M : Type u_4
β : Type u_5
inst✝⁵ : Semiring M
inst✝⁴ : AddCommMonoid α
inst✝³ : Module M α
inst✝² : ContinuousConstSMul M α
inst✝¹ : AddMonoid β
f : α →+ β
inst✝ : TopologicalSpace β
hf : IsQuotientMap ⇑f
n : ℕ
hc : IsUnit ↑n
⊢ IsUnit ↑n
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: α : Type u_2
inst✝⁶ : TopologicalSpace α
M : Type u_4
β : Type u_5
inst✝⁵ : Ring M
inst✝⁴ : AddCommGroup α
inst✝³ : Module M α
inst✝² : ContinuousConstSMul M α
inst✝¹ : AddGroup β
f : α →+ β
inst✝ : TopologicalSpace β
hf : IsQuotientMap ⇑f
n : ℤ
hc : IsUnit ↑n
⊢ IsUnit ↑n

Tactic:
]

Goal state after:
α : Type u_2
inst✝⁶ : TopologicalSpace α
M : Type u_4
β : Type u_5
inst✝⁵ : Ring M
inst✝⁴ : AddCommGroup α
inst✝³ : Module M α
inst✝² : ContinuousConstSMul M α
inst✝¹ : AddGroup β
f : α →+ β
inst✝ : TopologicalSpace β
hf : IsQuotientMap ⇑f
n : ℤ
hc : IsUnit ↑n
⊢ IsUnit ↑n
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: Γ : Type u_4
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : SMul Γ T
inst✝³ : ProperlyDiscontinuousSMul Γ T
inst✝² : T2Space T
inst✝¹ : LocallyCompactSpace T
inst✝ : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ | ((fun x ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite ↑Γ₀
u v : ↑Γ₀ → Set T
hu : ∀ (γ : ↑Γ₀), u γ ∈ 𝓝 (↑γ • x)
hv : ∀ (γ : ↑Γ₀), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : ↑Γ₀), Disjoint (u γ) (v γ)
γ : Γ
z : T
hz : z ∈ V ∧ ∀ (i : ↑Γ₀), z ∈ (fun x ↦ ↑i • x) ⁻¹' u i ∩ v i
hγz : (fun x ↦ γ • x) z ∈ V ∧ ∀ (i : ↑Γ₀), (fun x ↦ γ • x) z ∈ (fun x ↦ ↑i • x) ⁻¹' u i ∩ v i
h : ¬γ • x = x
⊢ False

Tactic:
]

Goal state after:
Γ : Type u_4
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : SMul Γ T
inst✝³ : ProperlyDiscontinuousSMul Γ T
inst✝² : T2Space T
inst✝¹ : LocallyCompactSpace T
inst✝ : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ | ((fun x ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite ↑Γ₀
u v : ↑Γ₀ → Set T
hu : ∀ (γ : ↑Γ₀), u γ ∈ 𝓝 (↑γ • x)
hv : ∀ (γ : ↑Γ₀), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : ↑Γ₀), Disjoint (u γ) (v γ)
γ : Γ
z : T
hz : z ∈ V ∧ ∀ (i : ↑Γ₀), z ∈ (fun x ↦ ↑i • x) ⁻¹' u i ∩ v i
hγz : (fun x ↦ γ • x) z ∈ V ∧ ∀ (i : ↑Γ₀), (fun x ↦ γ • x) z ∈ (fun x ↦ ↑i • x) ⁻¹' u i ∩ v i
h : ¬γ • x = x
⊢ False
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: Γ : Type u_4
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : SMul Γ T
inst✝³ : ProperlyDiscontinuousSMul Γ T
inst✝² : T2Space T
inst✝¹ : LocallyCompactSpace T
inst✝ : ContinuousConstSMul Γ T
x : T
x✝ : Set T
a✝ : Γ
⊢ ¬Disjoint ((fun x ↦ a✝ • x) '' x✝) x✝ → ¬a✝ • x ≠ x ↔ ((fun x ↦ a✝ • x) '' x✝ ∩ x✝).Nonempty → a✝ • x = x

Tactic:
]

Goal state after:
Γ : Type u_4
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : SMul Γ T
inst✝³ : ProperlyDiscontinuousSMul Γ T
inst✝² : T2Space T
inst✝¹ : LocallyCompactSpace T
inst✝ : ContinuousConstSMul Γ T
x : T
x✝ : Set T
a✝ : Γ
⊢ ¬Disjoint ((fun x ↦ a✝ • x) '' x✝) x✝ → ¬a✝ • x ≠ x ↔ ((fun x ↦ a✝ • x) '' x✝ ∩ x✝).Nonempty → a✝ • x = x
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: Γ : Type u_4
inst✝³ : Group Γ
T : Type u_5
inst✝² : TopologicalSpace T
inst✝¹ : MulAction Γ T
inst✝ : ContinuousConstSMul Γ T
U : Set T
hU : IsOpen[inst✝²] U
⊢ IsOpen[inst✝²] (⋃ g, (fun x ↦ g • x) '' U)

Tactic:
]

Goal state after:
Γ : Type u_4
inst✝³ : Group Γ
T : Type u_5
inst✝² : TopologicalSpace T
inst✝¹ : MulAction Γ T
inst✝ : ContinuousConstSMul Γ T
U : Set T
hU : IsOpen[inst✝²] U
⊢ IsOpen[inst✝²] (⋃ g, (fun x ↦ g • x) '' U)
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
⊢ Pairwise fun x y ↦ ∃ U ∈ 𝓝 x, ∃ V ∈ 𝓝 y, Disjoint U V

Tactic:
]

Goal state after:
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
⊢ Pairwise fun x y ↦ ∃ U ∈ 𝓝 x, ∃ V ∈ 𝓝 y, Disjoint U V
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : ContinuousMul M
a b : M
⊢ map (Function.uncurry fun x1 x2 ↦ x1 * x2) (𝓝 (a, b)) ≤ 𝓝 (a * b)

Tactic:
]

Goal state after:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : ContinuousMul M
a b : M
⊢ map (Function.uncurry fun x1 x2 ↦ x1 * x2) (𝓝 (a, b)) ≤ 𝓝 (a * b)
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : PosMulStrictMono 𝕜
h : Tendsto f l (𝓝[>] c)
x✝¹ : α
x✝ : c < f x✝¹
⊢ b * c < b * f x✝¹

Tactic:
]

Goal state after:
α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : PosMulStrictMono 𝕜
h : Tendsto f l (𝓝[>] c)
x✝¹ : α
x✝ : c < f x✝¹
⊢ b * c < b * f x✝¹
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : PosMulStrictMono 𝕜
h : Tendsto f l (𝓝[<] c)
x✝¹ : α
x✝ : f x✝¹ < c
⊢ b * f x✝¹ < b * c

Tactic:
]

Goal state after:
α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : PosMulStrictMono 𝕜
h : Tendsto f l (𝓝[<] c)
x✝¹ : α
x✝ : f x✝¹ < c
⊢ b * f x✝¹ < b * c
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : MulPosStrictMono 𝕜
h : Tendsto f l (𝓝[>] c)
x✝¹ : α
x✝ : c < f x✝¹
⊢ c * b < f x✝¹ * b

Tactic:
]

Goal state after:
α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : MulPosStrictMono 𝕜
h : Tendsto f l (𝓝[>] c)
x✝¹ : α
x✝ : c < f x✝¹
⊢ c * b < f x✝¹ * b
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : MulPosStrictMono 𝕜
h : Tendsto f l (𝓝[<] c)
x✝¹ : α
x✝ : f x✝¹ < c
⊢ f x✝¹ * b < c * b

Tactic:
]

Goal state after:
α : Type u_2
𝕜 : Type u_6
inst✝⁵ : Preorder 𝕜
inst✝⁴ : Zero 𝕜
inst✝³ : Mul 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : SeparatelyContinuousMul 𝕜
l : Filter α
f : α → 𝕜
b c : 𝕜
hb : 0 < b
inst✝ : MulPosStrictMono 𝕜
h : Tendsto f l (𝓝[<] c)
x✝¹ : α
x✝ : f x✝¹ < c
⊢ f x✝¹ * b < c * b
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
⊢ ∀ (x : M × M), ContinuousAt (fun p ↦ p.1 * p.2) x

Tactic:
]

Goal state after:
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
⊢ ∀ (x : M × M), ContinuousAt (fun p ↦ p.1 * p.2) x
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ map (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀) = map (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀)

Tactic:
]

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

Goal state before:
pp: M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ map (fun x ↦ (fun x1 x2 ↦ x1 * x2) (x₀ * x.1, x.2 * y₀).1 (x₀ * x.1, x.2 * y₀).2) (𝓝 1 ×ˢ 𝓝 1) =
    map (fun p ↦ x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1)

Tactic:
]

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

Goal state before:
pp: α : Type u_2
G₀ : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : AddMonoid α
inst✝² : DistribMulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
s : Set α
c : G₀
hc : c ≠ 0
⊢ c • s ∈ 𝓝 0 ↔ c • s ∈ 𝓝 0

Tactic:
]

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

Goal state before:
pp: M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ map ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) (map (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1)) =
    map ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) (map (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1))

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_4
us' : ι → UniformSpace G
h' : ∀ (i : ι), IsUniformGroup G
⊢ IsUniformGroup G

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Sort u_4
us' : ι → UniformSpace G
h' : ∀ (i : ι), IsUniformGroup G
⊢ IsUniformGroup G
Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions

Goal state before:
pp: G : Type u_1
inst✝ : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
⊢ IsUniformGroup G

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
⊢ IsUniformGroup G
Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions

Goal state before:
pp: G : Type u_1
H : Type u_2
hom : Type u_3
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : UniformSpace G
hG : IsUniformGroup G
inst✝ : UniformSpace H
hH : IsUniformGroup H
⊢ IsUniformGroup (G × H)

Tactic:
]

Goal state after:
G : Type u_1
H : Type u_2
hom : Type u_3
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : UniformSpace G
hG : IsUniformGroup G
inst✝ : UniformSpace H
hH : IsUniformGroup H
⊢ IsUniformGroup (G × H)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions

Goal state before:
pp: G✝ : Type u_1
H : Type u_2
hom : Type u_3
inst✝⁴ : Group G✝
inst✝³ : Group H
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → UniformSpace (G i)
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), IsUniformGroup (G i)
⊢ IsUniformGroup ((i : ι) → G i)

Tactic:
]

Goal state after:
G✝ : Type u_1
H : Type u_2
hom : Type u_3
inst✝⁴ : Group G✝
inst✝³ : Group H
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → UniformSpace (G i)
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), IsUniformGroup (G i)
⊢ IsUniformGroup ((i : ι) → G i)
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
⊢ ∀ (s : Set X) (y : Y), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
⊢ ∀ (s : Set X) (y : Y), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Continuous[inst✝¹, inst✝] f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ) ↔
    Continuous[inst✝¹, inst✝] f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Continuous[inst✝¹, inst✝] f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ) ↔
    Continuous[inst✝¹, inst✝] f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ 𝓝 (x₀ * y₀) = 𝓝 (x₀ * y₀)

Tactic:
]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hg : IsProperMap g
hf : IsProperMap f
ℱ : Filter X
z : Z
h : MapClusterPt z (map f ℱ) g
⊢ ∃ x, (g ∘ f) x = z ∧ ClusterPt x ℱ

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hg : IsProperMap g
hf : IsProperMap f
ℱ : Filter X
z : Z
h : MapClusterPt z (map f ℱ) g
⊢ ∃ x, (g ∘ f) x = z ∧ ClusterPt x ℱ
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsProperMap (g ∘ f)
f_surj : Surjective f
ℱ : Filter Y
z : Z
h : MapClusterPt z (comap f ℱ) (g ∘ f)
⊢ ∃ x, g x = z ∧ ClusterPt x ℱ

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsProperMap (g ∘ f)
f_surj : Surjective f
ℱ : Filter Y
z : Z
h : MapClusterPt z (comap f ℱ) (g ∘ f)
⊢ ∃ x, g x = z ∧ ClusterPt x ℱ
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsProperMap (g ∘ f)
f_surj : Surjective f
ℱ : Filter Y
x : X
hx : ClusterPt x (comap f ℱ)
h : MapClusterPt ((g ∘ f) x) (comap f ℱ) (g ∘ f)
⊢ ∃ x_1, g x_1 = (g ∘ f) x ∧ ClusterPt x_1 (map f (comap f ℱ))

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝¹, inst✝] g
hgf : IsProperMap (g ∘ f)
f_surj : Surjective f
ℱ : Filter Y
x : X
hx : ClusterPt x (comap f ℱ)
h : MapClusterPt ((g ∘ f) x) (comap f ℱ) (g ∘ f)
⊢ ∃ x_1, g x_1 = (g ∘ f) x ∧ ClusterPt x_1 (map f (comap f ℱ))
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
f : X → Y
g : Y → Z
inst✝ : T2Space Y
hf : Continuous[inst✝³, inst✝²] f
hg : Continuous[inst✝², inst✝¹] g
hgf : IsProperMap (g ∘ f)
⊢ Continuous[inst✝³, inst✝²] f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, ↑𝒰 ≤ 𝓝 x

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
f : X → Y
g : Y → Z
inst✝ : T2Space Y
hf : Continuous[inst✝³, inst✝²] f
hg : Continuous[inst✝², inst✝¹] g
hgf : IsProperMap (g ∘ f)
⊢ Continuous[inst✝³, inst✝²] f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, ↑𝒰 ≤ 𝓝 x
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
f : X → Y
g : Y → Z
inst✝ : T2Space Y
hf : Continuous[inst✝³, inst✝²] f
hg : Continuous[inst✝², inst✝¹] g
hgf :
  Continuous[inst✝³, inst✝¹] (g ∘ f) ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Z⦄, Tendsto (g ∘ f) (↑𝒰) (𝓝 y) → ∃ x, (g ∘ f) x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter X
y : Y
h : Tendsto f (↑𝒰) (𝓝 y)
⊢ ∃ x, ↑𝒰 ≤ 𝓝 x

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
f : X → Y
g : Y → Z
inst✝ : T2Space Y
hf : Continuous[inst✝³, inst✝²] f
hg : Continuous[inst✝², inst✝¹] g
hgf :
  Continuous[inst✝³, inst✝¹] (g ∘ f) ∧
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Z⦄, Tendsto (g ∘ f) (↑𝒰) (𝓝 y) → ∃ x, (g ∘ f) x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter X
y : Y
h : Tendsto f (↑𝒰) (𝓝 y)
⊢ ∃ x, ↑𝒰 ≤ 𝓝 x
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 * (V ∩ W) ∪ t * (V ∩ W) ⊆ U

Tactic:
]

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: case refine_4
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
this : ∃ t₁ ∈ 𝓝 x, ∃ t₂ ∈ 𝓝 0, t₁ ×ˢ t₂ ⊆ (fun p ↦ p.1 * p.2) ⁻¹' U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Tactic:
]

Goal state after:
case refine_4
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
this : ∃ t₁ ∈ 𝓝 x, ∃ t₂ ∈ 𝓝 0, t₁ ×ˢ t₂ ⊆ (fun p ↦ p.1 * p.2) ⁻¹' U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case refine_4
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
t : Set M
ht : t ∈ 𝓝 x
s : Set M
hs : s ∈ 𝓝 0
h : t * s ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Tactic:
]

Goal state after:
case refine_4
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
t : Set M
ht : t ∈ 𝓝 x
s : Set M
hs : s ∈ 𝓝 0
h : t * s ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U