awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
L : ∀ x ∈ s, ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ ContinuousOn f s

Tactic:
fun x hx =>
  continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt hx (L x hx)

Premises used: continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt, ContinuousOn
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
L : ∀ u ∈ 𝓤 β, ∃ (F : α → β), ContinuousOn F s ∧ ∀ y ∈ s, (f y, F y) ∈ u
⊢ ContinuousOn f s

Tactic:
continuousOn_of_locally_uniform_approx_of_continuousWithinAt fun _x hx u hu =>
    ⟨s, self_mem_nhdsWithin, (L u hu).imp fun _F hF => ⟨hF.1.continuousWithinAt hx, hF.2⟩⟩

Premises used: Exists.imp, self_mem_nhdsWithin, And.intro, Exists.intro, continuousOn_of_locally_uniform_approx_of_continuousWithinAt
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : α → β
L : ∀ (x : α), ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ (F : α → β), ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ Continuous[inst, inst_1.toTopologicalSpace] f

Tactic:
continuous_iff_continuousAt.2 fun x =>
    continuousAt_of_locally_uniform_approx_of_continuousAt (L x)

Premises used: Iff.mpr, continuous_iff_continuousAt, continuousAt_of_locally_uniform_approx_of_continuousAt
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : α → β
L : ∀ u ∈ 𝓤 β, ∃ (F : α → β), Continuous[inst, inst_1.toTopologicalSpace] F ∧ ∀ (y : α), (f y, F y) ∈ u
⊢ ∀ u ∈ 𝓤 β, ∃ (F : α → β), ContinuousOn F univ ∧ ∀ (y : α), Membership.mem (γ := Set α) univ y → (f y, F y) ∈ u

Tactic:
simpa [continuousOn_univ] using L

Premises used: continuousOn_univ
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
hc : ∃ᶠ (n : ι) in p, ContinuousOn (F n) s
⊢ ContinuousOn f s

Tactic:
continuousOn_of_locally_uniform_approx_of_continuousWithinAt fun x hx u hu => ?_

Premises used: continuousOn_of_locally_uniform_approx_of_continuousWithinAt
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
hc : ∃ᶠ (n : ι) in p, ContinuousOn (F n) s
refine :
  ∀ (x : α) (hx : x ∈ s) (u : Set (β × β)) (hu : u ∈ 𝓤 β),
    ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ ContinuousOn f s

Tactic:
refine continuousOn_of_locally_uniform_approx_of_continuousWithinAt fun x hx u hu => ?_

Premises used: continuousOn_of_locally_uniform_approx_of_continuousWithinAt
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
hc : ∃ᶠ (n : ι) in p, ContinuousOn (F n) s
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
rcases :
  ∀ (t : Set α) (ht : t ∈ 𝓝[s] x) (H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u),
    ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u

Tactic:
rcases h u hu x hx with ⟨t, ht, H⟩
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
hc : ∃ᶠ (n : ι) in p, ContinuousOn (F n) s
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
rcases :
  ∀ (n : ι) (hFc : ContinuousOn (F n) s) (hF : ∀ y ∈ t, (f y, F n y) ∈ u),
    ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u

Tactic:
rcases (hc.and_eventually H).exists with ⟨n, hFc, hF⟩

Premises used: Filter.Frequently.and_eventually, Filter.Frequently.exists
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
hc : ∃ᶠ (n : ι) in p, ContinuousOn (F n) s
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
n : ι
hFc : ContinuousOn (F n) s
hF : ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u

Tactic:
⟨t, ht, ⟨F n, hFc.continuousWithinAt hx, hF⟩⟩

Premises used: And.intro, Exists.intro, ContinuousOn.continuousWithinAt
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
hc : ∃ᶠ (n : ι) in p, ContinuousOn (F n) s
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
n : ι
hFc : ContinuousOn (F n) s
hF : ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u

Tactic:
exact ⟨t, ht, ⟨F n, hFc.continuousWithinAt hx, hF⟩⟩
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoUniformlyOn F f p s
hc : ∃ᶠ (n : ι) in p, ContinuousOn (F n) s
⊢ ContinuousOn f s

Tactic:
h.tendstoLocallyUniformlyOn.continuousOn hc

Premises used: TendstoLocallyUniformlyOn.continuousOn, TendstoUniformlyOn.tendstoLocallyUniformlyOn
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : TendstoLocallyUniformly F f p
hc : ∃ᶠ (n : ι) in p, Continuous[inst, inst_1.toTopologicalSpace] (F n)
⊢ Continuous[inst, inst_1.toTopologicalSpace] f

Tactic:
continuousOn_univ.mp <|
    h.tendstoLocallyUniformlyOn.continuousOn <| hc.mono fun _n hn => hn.continuousOn

Premises used: Continuous.continuousOn, TendstoLocallyUniformly.tendstoLocallyUniformlyOn, TendstoLocallyUniformlyOn.continuousOn, Filter.Frequently.mono, Iff.mp, continuousOn_univ
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : TendstoUniformly F f p
hc : ∃ᶠ (n : ι) in p, Continuous[inst, inst_1.toTopologicalSpace] (F n)
⊢ Continuous[inst, inst_1.toTopologicalSpace] f

Tactic:
h.tendstoLocallyUniformly.continuous hc

Premises used: TendstoLocallyUniformly.continuous, TendstoUniformly.tendstoLocallyUniformly
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f s x
hg : Tendsto g p (𝓝[s] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun (n : ι) ↦ F n (g n)) p (𝓝 (f x))

Tactic:
Uniform.tendsto_nhds_right.2 fun u₀ hu₀ => ?_

Premises used: Iff.mpr, Uniform.tendsto_nhds_right
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f s x
hg : Tendsto g p (𝓝[s] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
refine :
  ∀ (u₀ : Set (β × β)) (hu₀ : u₀ ∈ 𝓤 β),
    Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : ι) ↦ (f x, F x_1 (g x_1))) p) u₀
⊢ Tendsto (fun (n : ι) ↦ F n (g n)) p (𝓝 (f x))

Tactic:
refine Uniform.tendsto_nhds_right.2 fun u₀ hu₀ => ?_

Premises used: Iff.mpr, Uniform.tendsto_nhds_right
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f s x
hg : Tendsto g p (𝓝[s] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
⊢ ∃ u ∈ 𝓤 β, u ○ u ⊆ u₀

Tactic:
comp_mem_uniformity_sets hu₀

Premises used: comp_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f s x
hg : Tendsto g p (𝓝[s] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
obtain :
  ∀ (u₁ : Set (β × β)) (h₁ : u₁ ∈ 𝓤 β) (u₁₀ : u₁ ○ u₁ ⊆ u₀),
    Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : ι) ↦ (f x, F x_1 (g x_1))) p) u₀
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : ι) ↦ (f x, F x_1 (g x_1))) p) u₀

Tactic:
obtain ⟨u₁, h₁, u₁₀⟩ : ∃ u ∈ 𝓤 β, u ○ u ⊆ u₀ := comp_mem_uniformity_sets hu₀

Premises used: uniformity, comp_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f s x
hg : Tendsto g p (𝓝[s] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
rcases :
  ∀ (s_1 : Set α) (sx : s_1 ∈ 𝓝[s] x) (hs : ∀ᶠ (n : ι) in p, ∀ y ∈ s_1, (f y, F n y) ∈ u₁),
    Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : ι) ↦ (f x, F x_1 (g x_1))) p) u₀
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : ι) ↦ (f x, F x_1 (g x_1))) p) u₀

Tactic:
rcases hunif u₁ h₁ with ⟨s, sx, hs⟩
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s_1 : Set α
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f s_1 x
hg : Tendsto g p (𝓝[s_1] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s_1] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
s : Set α
sx : s ∈ 𝓝[s_1] x
hs : ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, F n y) ∈ u₁
⊢ ∀ᶠ (n : ι) in p, g n ∈ s

Tactic:
have A : ∀ᶠ n in p, g n ∈ s := hg sx
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s_1 : Set α
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f s_1 x
hg : Tendsto g p (𝓝[s_1] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s_1] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
s : Set α
sx : s ∈ 𝓝[s_1] x
hs : ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, F n y) ∈ u₁
A : ∀ᶠ (n : ι) in p, g n ∈ s
⊢ ∀ᶠ (n : ι) in p, (f x, f (g n)) ∈ u₁

Tactic:
have B : ∀ᶠ n in p, (f x, f (g n)) ∈ u₁ := hg (Uniform.continuousWithinAt_iff'_right.1 h h₁)
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s_1 : Set α
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f s_1 x
hg : Tendsto g p (𝓝[s_1] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s_1] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
s : Set α
sx : s ∈ 𝓝[s_1] x
hs : ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, F n y) ∈ u₁
A : ∀ᶠ (n : ι) in p, g n ∈ s
B : ∀ᶠ (n : ι) in p, (f x, f (g n)) ∈ u₁
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : ι) ↦ (f x, F x_1 (g x_1))) p) u₀

Tactic:
B.mp <| A.mp <| hs.mono fun y H1 H2 H3 => u₁₀ <| prodMk_mem_comp H3 <| H1 _ H2

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.Eventually.mono, Filter.Eventually.mp, Set.preimage, SetRel.prodMk_mem_comp
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s_1 : Set α
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f s_1 x
hg : Tendsto g p (𝓝[s_1] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s_1] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
s : Set α
sx : s ∈ 𝓝[s_1] x
hs : ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, F n y) ∈ u₁
A : ∀ᶠ (n : ι) in p, g n ∈ s
B : ∀ᶠ (n : ι) in p, (f x, f (g n)) ∈ u₁
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : ι) ↦ (f x, F x_1 (g x_1))) p) u₀

Tactic:
exact B.mp <| A.mp <| hs.mono fun y H1 H2 H3 => u₁₀ <| prodMk_mem_comp H3 <| H1 _ H2

Premises used: Filter.Eventually.mono, Filter.Eventually.mp
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
h : ContinuousAt f x
hg : Tendsto g p (𝓝 x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ContinuousWithinAt f univ x

Tactic:
rw [← continuousWithinAt_univ] at h

Premises used: continuousWithinAt_univ
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
h : ContinuousAt f x
hg : Tendsto g p (𝓝 x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
h₁ : ContinuousWithinAt f univ x
⊢ Tendsto g p (𝓝 x)

Tactic:
rw [← continuousWithinAt_univ] at h

Premises used: continuousWithinAt_univ
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
h : ContinuousAt f x
hg : Tendsto g p (𝓝 x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
h₁ : ContinuousWithinAt f univ x
hg₁ : Tendsto g p (𝓝 x)
⊢ ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
rw [← continuousWithinAt_univ] at h

Premises used: continuousWithinAt_univ
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : 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 g p (𝓝[univ] x)

Tactic:
rw [← nhdsWithin_univ] at hunif hg

Premises used: nhdsWithin_univ
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : 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
hg₁ : Tendsto g p (𝓝[univ] x)
⊢ ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[univ] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
rw [← nhdsWithin_univ] at hunif hg

Premises used: nhdsWithin_univ
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : 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:
tendsto_comp_of_locally_uniform_limit_within h hg hunif

Premises used: tendsto_comp_of_locally_uniform_limit_within
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : 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:
exact tendsto_comp_of_locally_uniform_limit_within h hg hunif

Premises used: tendsto_comp_of_locally_uniform_limit_within
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
x : α
p : Filter ι
g : ι → α
h : TendstoLocallyUniformlyOn F f p s
hf : ContinuousWithinAt f s x
hx : x ∈ s
hg : Tendsto g p (𝓝[s] x)
⊢ Tendsto (fun (n : ι) ↦ F n (g n)) p (𝓝 (f x))

Tactic:
tendsto_comp_of_locally_uniform_limit_within hf hg fun u hu => h u hu x hx

Premises used: tendsto_comp_of_locally_uniform_limit_within
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
x : α
p : Filter ι
g : ι → α
h : TendstoUniformlyOn F f p s
hf : ContinuousWithinAt f s x
hg : Tendsto g p (𝓝[s] x)
⊢ Tendsto (fun (n : ι) ↦ F n (g n)) p (𝓝 (f x))

Tactic:
tendsto_comp_of_locally_uniform_limit_within hf hg fun u hu => ⟨s, self_mem_nhdsWithin, h u hu⟩

Premises used: self_mem_nhdsWithin, And.intro, Exists.intro, tendsto_comp_of_locally_uniform_limit_within
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
h : TendstoLocallyUniformly F f p
hf : ContinuousAt f x
hg : Tendsto g p (𝓝 x)
⊢ Tendsto (fun (n : ι) ↦ F n (g n)) p (𝓝 (f x))

Tactic:
tendsto_comp_of_locally_uniform_limit hf hg fun u hu => h u hu x

Premises used: tendsto_comp_of_locally_uniform_limit
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
h : TendstoUniformly F f p
hf : ContinuousAt f x
hg : Tendsto g p (𝓝 x)
⊢ Tendsto (fun (n : ι) ↦ F n (g n)) p (𝓝 (f x))

Tactic:
h.tendstoLocallyUniformly.tendsto_comp hf hg

Premises used: TendstoUniformly.tendstoLocallyUniformly, TendstoLocallyUniformly.tendsto_comp
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_4
β : Type u_5
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
h : ∀ u ∈ 𝓤 β, ∃ (F : α → β), UniformContinuousOn F s ∧ ∀ y ∈ s, (f y, F y) ∈ u
simp_rw :
  ∀
    (h :
      ∀ u ∈ 𝓤 β,
        ∃ (F : α → β),
          (∀ r ∈ 𝓤 β,
              Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
                {x : (↑s : Type u_4) × (↑s : Type u_4) |
                  (s.restrict (π := fun (a : α) ↦ β) F x.1, s.restrict (π := fun (a : α) ↦ β) F x.2) ∈ r}) ∧
            ∀ y ∈ s, (f y, F y) ∈ u),
    ∀ r ∈ 𝓤 β,
      Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
        {x : (↑s : Type u_4) × (↑s : Type u_4) |
          (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2) ∈ r}
⊢ UniformContinuousOn f s

Tactic:
simp_rw [uniformContinuousOn_iff_restrict, uniformContinuous_def] at h ⊢

Premises used: uniformContinuous_def, uniformContinuousOn_iff_restrict
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_4
β : Type u_5
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
h :
  ∀ u ∈ 𝓤 β,
    ∃ (F : α → β),
      (∀ r ∈ 𝓤 β,
          Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
            {x : (↑s : Type u_4) × (↑s : Type u_4) |
              (s.restrict (π := fun (a : α) ↦ β) F x.1, s.restrict (π := fun (a : α) ↦ β) F x.2) ∈ r}) ∧
        ∀ y ∈ s, (f y, F y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
obtain :
  ∀ (v : Set (β × β)) (hv : v ∈ 𝓤 β) (hvsymm : SetRel.IsSymm v) (hvu : v ○ v ○ v ⊆ u),
    Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
      {x : (↑s : Type u_4) × (↑s : Type u_4) |
        (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2) ∈ u}
⊢ Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
    {x : (↑s : Type u_4) × (↑s : Type u_4) |
      (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2) ∈ u}

Tactic:
obtain ⟨v, hv, hvsymm, hvu⟩ := comp_comp_symm_mem_uniformity_sets hu

Premises used: comp_comp_symm_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_4
β : Type u_5
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
h :
  ∀ u ∈ 𝓤 β,
    ∃ (F : α → β),
      (∀ r ∈ 𝓤 β,
          Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
            {x : (↑s : Type u_4) × (↑s : Type u_4) |
              (s.restrict (π := fun (a : α) ↦ β) F x.1, s.restrict (π := fun (a : α) ↦ β) F x.2) ∈ r}) ∧
        ∀ y ∈ s, (f y, F y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
v : Set (β × β)
hv : v ∈ 𝓤 β
hvsymm : SetRel.IsSymm v
hvu : v ○ v ○ v ⊆ u
obtain :
  ∀ (F : α → β)
    (hF :
      ∀ r ∈ 𝓤 β,
        Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
          {x : (↑s : Type u_4) × (↑s : Type u_4) |
            (s.restrict (π := fun (a : α) ↦ β) F x.1, s.restrict (π := fun (a : α) ↦ β) F x.2) ∈ r})
    (hFv : ∀ y ∈ s, (f y, F y) ∈ v),
    Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
      {x : (↑s : Type u_4) × (↑s : Type u_4) |
        (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2) ∈ u}
⊢ Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
    {x : (↑s : Type u_4) × (↑s : Type u_4) |
      (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2) ∈ u}

Tactic:
obtain ⟨F, hF, hFv⟩ := h v hv
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_4
β : Type u_5
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
h :
  ∀ u ∈ 𝓤 β,
    ∃ (F : α → β),
      (∀ r ∈ 𝓤 β,
          Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
            {x : (↑s : Type u_4) × (↑s : Type u_4) |
              (s.restrict (π := fun (a : α) ↦ β) F x.1, s.restrict (π := fun (a : α) ↦ β) F x.2) ∈ r}) ∧
        ∀ y ∈ s, (f y, F y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
v : Set (β × β)
hv : v ∈ 𝓤 β
hvsymm : SetRel.IsSymm v
hvu : v ○ v ○ v ⊆ u
F : α → β
hF :
  ∀ r ∈ 𝓤 β,
    Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
      {x : (↑s : Type u_4) × (↑s : Type u_4) |
        (s.restrict (π := fun (a : α) ↦ β) F x.1, s.restrict (π := fun (a : α) ↦ β) F x.2) ∈ r}
hFv : ∀ y ∈ s, (f y, F y) ∈ v
h₁ :
  ∀ (x : (↑s : Type u_4) × (↑s : Type u_4))
    (hx : (s.restrict (π := fun (a : α) ↦ β) F x.1, s.restrict (π := fun (a : α) ↦ β) F x.2) ∈ v),
    (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2) ∈ u
⊢ Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
    {x : (↑s : Type u_4) × (↑s : Type u_4) |
      (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2) ∈ u}

Tactic:
filter_upwards [hF v hv] with x hx