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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
ht : univ ⊆ ⋃ x ∈ t, U ↑x
hU : ∀ᶠ (x : ι) in p, ∀ (i : ↥t), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
ht : univ ⊆ ⋃ x ∈ t, U ↑x
hU : ∀ᶠ (x : ι) in p, ∀ (i : ↥t), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hs : IsCompact s
this : CompactSpace ↑s
h : TendstoUniformlyOn F f p s
⊢ TendstoUniformlyOn F f p s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hs : IsCompact s
this : CompactSpace ↑s
h : TendstoUniformlyOn F f p s
⊢ TendstoUniformlyOn F f p s
Module: Mathlib.Topology.UniformSpace.UniformApproximation

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝 x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun n ↦ F n (g n)) p (𝓝 (f x))

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝 x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun n ↦ F n (g n)) p (𝓝 (f x))
Module: Mathlib.Topology.UniformSpace.UniformApproximation

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝[univ] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[univ] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun n ↦ F n (g n)) p (𝓝 (f x))

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝[univ] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[univ] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun n ↦ F n (g n)) p (𝓝 (f x))
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformlyOn F f p univ
g : γ → α
cg : Continuous[inst✝, inst✝²] g
⊢ TendstoLocallyUniformlyOn (fun n ↦ F n ∘ g) (f ∘ g) p univ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformlyOn F f p univ
g : γ → α
cg : Continuous[inst✝, inst✝²] g
⊢ TendstoLocallyUniformlyOn (fun n ↦ F n ∘ g) (f ∘ g) p univ
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformlyOn F f p univ
g : γ → α
cg : ContinuousOn g univ
⊢ TendstoLocallyUniformlyOn (fun n ↦ F n ∘ g) (f ∘ g) p univ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformlyOn F f p univ
g : γ → α
cg : ContinuousOn g univ
⊢ TendstoLocallyUniformlyOn (fun n ↦ F n ∘ g) (f ∘ g) p univ
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : UniformSpace γ
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hfs : MapsTo f s t
hFs : ∀ᶠ (n : ι) in p, MapsTo (F n) s t
⊢ ∀ x ∈ s, Tendsto (fun y ↦ ((g ∘ f) y.2, (g ∘ F y.1) y.2)) (p ×ˢ 𝓝[s] x) (𝓤 γ)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : UniformSpace γ
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hfs : MapsTo f s t
hFs : ∀ᶠ (n : ι) in p, MapsTo (F n) s t
⊢ ∀ x ∈ s, Tendsto (fun y ↦ ((g ∘ f) y.2, (g ∘ F y.1) y.2)) (p ×ˢ 𝓝[s] x) (𝓤 γ)
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : UniformSpace γ
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : TendstoLocallyUniformlyOn F f p univ
hfs : ∀ (x : α), f x ∈ t
hFs : ∀ᶠ (n : ι) in p, ∀ (x : α), F n x ∈ t
⊢ TendstoLocallyUniformlyOn (fun x ↦ g ∘ F x) (g ∘ f) p univ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : UniformSpace γ
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : TendstoLocallyUniformlyOn F f p univ
hfs : ∀ (x : α), f x ∈ t
hFs : ∀ᶠ (n : ι) in p, ∀ (x : α), F n x ∈ t
⊢ TendstoLocallyUniformlyOn (fun x ↦ g ∘ F x) (g ∘ f) p univ
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
f : α → β
h : Continuous[inst✝².toTopologicalSpace, inst✝¹.toTopologicalSpace] f
⊢ map (Prod.map f f) (𝓤 α) = map (Prod.map f f) (𝓤 α)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
⊢ UniformContinuous (s.domRestrict f)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
⊢ UniformContinuous (s.domRestrict f)
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace ↑s
hf : ContinuousOn f s
⊢ UniformContinuous (s.domRestrict f)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace ↑s
hf : ContinuousOn f s
⊢ UniformContinuous (s.domRestrict f)
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace ↑s
hf : Continuous[instTopologicalSpaceSubtype, inst✝.toTopologicalSpace] (s.domRestrict f)
⊢ UniformContinuous (s.domRestrict f)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace ↑s
hf : Continuous[instTopologicalSpaceSubtype, inst✝.toTopologicalSpace] (s.domRestrict f)
⊢ UniformContinuous (s.domRestrict f)
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 γ)
⊢ ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 (β × γ))

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 γ)
⊢ ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 (β × γ))
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 γ)
x : α
hx : x ∈ s
⊢ Tendsto ((fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x)
    (𝓤 β ×ˢ 𝓤 γ)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 γ)
x : α
hx : x ∈ s
⊢ Tendsto ((fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x)
    (𝓤 β ×ˢ 𝓤 γ)
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : TendstoLocallyUniformlyOn F f p univ
hG : TendstoLocallyUniformlyOn G g p univ
⊢ TendstoLocallyUniformlyOn (fun n x ↦ (F n x, G n x)) (fun x ↦ (f x, g x)) p univ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : TendstoLocallyUniformlyOn F f p univ
hG : TendstoLocallyUniformlyOn G g p univ
⊢ TendstoLocallyUniformlyOn (fun n x ↦ (F n x, G n x)) (fun x ↦ (f x, g x)) p univ
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, TendstoUniformlyOn F f p t
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝[s] x
htr : Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 t) (𝓤 β)
⊢ Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, TendstoUniformlyOn F f p t
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝[s] x
htr : Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 t) (𝓤 β)
⊢ Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_4
F : ι → β → α
inst✝ : CompactSpace β
h : Continuous[inst✝¹.toTopologicalSpace, UniformFun.topologicalSpace ι α] (⇑UniformFun.ofFun ∘ Function.swap F)
⊢ UniformEquicontinuous F

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_4
F : ι → β → α
inst✝ : CompactSpace β
h : Continuous[inst✝¹.toTopologicalSpace, UniformFun.topologicalSpace ι α] (⇑UniformFun.ofFun ∘ Function.swap F)
⊢ UniformEquicontinuous F
Module: Mathlib.Topology.UniformSpace.HeineCantor

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_4
F : ι → β → α
inst✝ : CompactSpace β
h : Continuous[inst✝¹.toTopologicalSpace, UniformFun.topologicalSpace ι α] (⇑UniformFun.ofFun ∘ Function.swap F)
⊢ UniformContinuous (⇑UniformFun.ofFun ∘ Function.swap F)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_4
F : ι → β → α
inst✝ : CompactSpace β
h : Continuous[inst✝¹.toTopologicalSpace, UniformFun.topologicalSpace ι α] (⇑UniformFun.ofFun ∘ Function.swap F)
⊢ UniformContinuous (⇑UniformFun.ofFun ∘ Function.swap F)
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ max (a / b) (a / c) = a / min b c

Tactic:
simp only [div_eq_mul_inv, max_mul_mul_left, max_inv_inv']

Goal state after:
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ max c d - max a b ≤ max |c - a| |d - b|

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ max c d - max a b ≤ max |c - a| |d - b|
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ (∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U) ↔
    ∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U

Tactic:
]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
⊢ (∀ U ∈ 𝓤 α, ∀ᶠ (xy : ↑S × ↑S) in 𝓤 ↑S, ∀ (i : ι), ((S.domRestrict ∘ F) i xy.1, (S.domRestrict ∘ F) i xy.2) ∈ U) ↔
    ∀ U ∈ 𝓤 α, ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ U

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
⊢ (∀ U ∈ 𝓤 α, ∀ᶠ (xy : ↑S × ↑S) in 𝓤 ↑S, ∀ (i : ι), ((S.domRestrict ∘ F) i xy.1, (S.domRestrict ∘ F) i xy.2) ∈ U) ↔
    ∀ U ∈ 𝓤 α, ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ U
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg✝ : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)
⊢ ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg✝ : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)
⊢ ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf✝ : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg✝ : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)
x : α
hx : x ∈ s
hf :
  ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, F x.1 x.2) ∈ id i
⊢ ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, G x.1 x.2) ∈ id i

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf✝ : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg✝ : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)
x : α
hx : x ∈ s
hf :
  ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, F x.1 x.2) ∈ id i
⊢ ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, G x.1 x.2) ∈ id i
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ x ∈ s, Inseparable (f x) (g x)
⊢ ∀ᶠ (x : ι) in p, ∀ y ∈ s, Inseparable (f (x, y).2) (g (x, y).2)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ x ∈ s, Inseparable (f x) (g x)
⊢ ∀ᶠ (x : ι) in p, ∀ y ∈ s, Inseparable (f (x, y).2) (g (x, y).2)
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg✝ : ∀ x ∈ s, Inseparable (f x) (g x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)
⊢ ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg✝ : ∀ x ∈ s, Inseparable (f x) (g x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)
⊢ ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf✝ : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg✝ : ∀ x ∈ s, Inseparable (f x) (g x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)
x : α
hx : x ∈ s
hf :
  ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, F x.1 x.2) ∈ id i
⊢ ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (g x.2, F x.1 x.2) ∈ id i

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf✝ : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg✝ : ∀ x ∈ s, Inseparable (f x) (g x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)
x : α
hx : x ∈ s
hf :
  ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, F x.1 x.2) ∈ id i
⊢ ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (g x.2, F x.1 x.2) ∈ id i
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets

Tactic:
]

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
x : α
⊢ ∀ i' ∈ 𝓤 β,
    ∃ i ∈ 𝓤 β,
      UniformFun.gen α β i ⊆ (fun x_1 ↦ ((Function.eval x ∘ ⇑toFun) x_1.1, (Function.eval x ∘ ⇑toFun) x_1.2)) ⁻¹' id i'

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
x : α
⊢ ∀ i' ∈ 𝓤 β,
    ∃ i ∈ 𝓤 β,
      UniformFun.gen α β i ⊆ (fun x_1 ↦ ((Function.eval x ∘ ⇑toFun) x_1.1, (Function.eval x ∘ ⇑toFun) x_1.2)) ⁻¹' id i'
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
⊢ UniformFun.filter α γ (⨅ i, 𝓤 γ) = ⨅ i, 𝓤 (α →ᵤ γ)

Tactic:
]

Goal state after:
α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
⊢ UniformFun.filter α γ (⨅ i, 𝓤 γ) = ⨅ i, 𝓤 (α →ᵤ γ)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
⊢ ⨅ i, uniformSpace α γ = ⨅ b, bif b then uniformSpace α γ else uniformSpace α γ

Tactic:
]

Goal state after:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
⊢ ⨅ i, uniformSpace α γ = ⨅ b, bif b then uniformSpace α γ else uniformSpace α γ
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
⊢ EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt Subtype.val S x₀

Tactic:
simp only [EquicontinuousWithinAt, forall_subtype_range_iff]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
h : UniformEquicontinuous F
⊢ UniformEquicontinuous (F ∘ rangeSplitting F)

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
h : UniformEquicontinuous F
⊢ UniformEquicontinuous (F ∘ rangeSplitting F)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
h : UniformEquicontinuousOn F S
⊢ UniformEquicontinuousOn (F ∘ rangeSplitting F) S

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
h : UniformEquicontinuousOn F S
⊢ UniformEquicontinuousOn (F ∘ rangeSplitting F) S
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
f : γ → α
⊢ ∀ ib ∈ 𝓤 β,
    ∃ ia ∈ 𝓤 β, ∀ x ∈ UniformFun.gen α β ia, (ofFun (toFun x.1 ∘ f), ofFun (toFun x.2 ∘ f)) ∈ UniformFun.gen γ β ib

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
f : γ → α
⊢ ∀ ib ∈ 𝓤 β,
    ∃ ia ∈ 𝓤 β, ∀ x ∈ UniformFun.gen α β ia, (ofFun (toFun x.1 ∘ f), ofFun (toFun x.2 ∘ f)) ∈ UniformFun.gen γ β ib
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔
    ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝 x₀, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α i}

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔
    ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝 x₀, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α i}