[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ TendstoUniformlyOn F f p s ↔ TendstoUniformlyOnFilter F f p (𝓟 s)
[PROOFSTEP]
simp only [TendstoUniformlyOn, TendstoUniformlyOnFilter]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ (∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (n : ι) in p, ∀ (x : α), x ∈ s → (f x, F n x) ∈ u) ↔
    ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, (f n.snd, F n.fst n.snd) ∈ u
[PROOFSTEP]
apply forall₂_congr
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ ∀ (a : Set (β × β)),
    a ∈ 𝓤 β →
      ((∀ᶠ (n : ι) in p, ∀ (x : α), x ∈ s → (f x, F n x) ∈ a) ↔
        ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, (f n.snd, F n.fst n.snd) ∈ a)
[PROOFSTEP]
simp_rw [eventually_prod_principal_iff]
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ ∀ (a : Set (β × β)), a ∈ 𝓤 β → True
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F✝ : ι → α → β
f✝ : α → β
s✝ s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g : ι → α
F : ι → α → β
f : α → β
p : Filter ι
s : Set α
⊢ TendstoUniformlyOn F f p s ↔ Tendsto (fun q => (f q.snd, F q.fst q.snd)) (p ×ˢ 𝓟 s) (𝓤 β)
[PROOFSTEP]
simp [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, tendstoUniformlyOnFilter_iff_tendsto]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ TendstoUniformlyOn F f p univ ↔ TendstoUniformly F f p
[PROOFSTEP]
simp [TendstoUniformlyOn, TendstoUniformly]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ TendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤
[PROOFSTEP]
rw [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, principal_univ]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
h : TendstoUniformly F f p
⊢ TendstoUniformlyOnFilter F f p ⊤
[PROOFSTEP]
rwa [← tendstoUniformly_iff_tendstoUniformlyOnFilter]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
u : Set (β × β)
x✝ : u ∈ 𝓤 β
⊢ (∀ᶠ (n : ι) in p, ∀ (x : α), x ∈ s → (f x, F n x) ∈ u) ↔
    ∀ᶠ (n : ι) in p, ∀ (x : ↑s), ((f ∘ Subtype.val) x, (fun i x => F i ↑x) n x) ∈ u
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F✝ : ι → α → β
f✝ : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g : ι → α
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoUniformly F f p ↔ Tendsto (fun q => (f q.snd, F q.fst q.snd)) (p ×ˢ ⊤) (𝓤 β)
[PROOFSTEP]
simp [tendstoUniformly_iff_tendstoUniformlyOnFilter, tendstoUniformlyOnFilter_iff_tendsto]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
h : TendstoUniformlyOnFilter F f p p'
hx : 𝓟 {x} ≤ p'
⊢ Tendsto (fun n => F n x) p (𝓝 (f x))
[PROOFSTEP]
refine' Uniform.tendsto_nhds_right.mpr fun u hu => mem_map.mpr _
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
h : TendstoUniformlyOnFilter F f p p'
hx : 𝓟 {x} ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ (fun x_1 => (f x, F x_1 x)) ⁻¹' u ∈ p
[PROOFSTEP]
filter_upwards [(h u hu).curry]
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
h : TendstoUniformlyOnFilter F f p p'
hx : 𝓟 {x} ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ (a : ι), (∀ᶠ (y : α) in p', (f y, F a y) ∈ u) → a ∈ (fun x_1 => (f x, F x_1 x)) ⁻¹' u
[PROOFSTEP]
intro i h
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
h✝ : TendstoUniformlyOnFilter F f p p'
hx : 𝓟 {x} ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
i : ι
h : ∀ᶠ (y : α) in p', (f y, F i y) ∈ u
⊢ i ∈ (fun x_1 => (f x, F x_1 x)) ⁻¹' u
[PROOFSTEP]
simpa using h.filter_mono hx
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p p'
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.fst n.snd = F' n.fst n.snd
⊢ TendstoUniformlyOnFilter F' f p p'
[PROOFSTEP]
refine' fun u hu => ((hf u hu).and hff').mono fun n h => _
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p p'
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.fst n.snd = F' n.fst n.snd
u : Set (β × β)
hu : u ∈ 𝓤 β
n : ι × α
h : (f n.snd, F n.fst n.snd) ∈ u ∧ F n.fst n.snd = F' n.fst n.snd
⊢ (f n.snd, F' n.fst n.snd) ∈ u
[PROOFSTEP]
rw [← h.right]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p p'
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.fst n.snd = F' n.fst n.snd
u : Set (β × β)
hu : u ∈ 𝓤 β
n : ι × α
h : (f n.snd, F n.fst n.snd) ∈ u ∧ F n.fst n.snd = F' n.fst n.snd
⊢ (f n.snd, F n.fst n.snd) ∈ u
[PROOFSTEP]
exact h.left
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
F' : ι → α → β
hf : TendstoUniformlyOn F f p s
hff' : ∀ᶠ (n : ι) in p, EqOn (F n) (F' n) s
⊢ TendstoUniformlyOn F' f p s
[PROOFSTEP]
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter] at hf ⊢
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p (𝓟 s)
hff' : ∀ᶠ (n : ι) in p, EqOn (F n) (F' n) s
⊢ TendstoUniformlyOnFilter F' f p (𝓟 s)
[PROOFSTEP]
refine' hf.congr _
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p (𝓟 s)
hff' : ∀ᶠ (n : ι) in p, EqOn (F n) (F' n) s
⊢ ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, F n.fst n.snd = F' n.fst n.snd
[PROOFSTEP]
rw [eventually_iff] at hff' ⊢
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p (𝓟 s)
hff' : {x | EqOn (F x) (F' x) s} ∈ p
⊢ {x | F x.fst x.snd = F' x.fst x.snd} ∈ p ×ˢ 𝓟 s
[PROOFSTEP]
simp only [Set.EqOn] at hff' 
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p (𝓟 s)
hff' : {x | ∀ ⦃x_1 : α⦄, x_1 ∈ s → F x x_1 = F' x x_1} ∈ p
⊢ {x | F x.fst x.snd = F' x.fst x.snd} ∈ p ×ˢ 𝓟 s
[PROOFSTEP]
simp only [mem_prod_principal, hff', mem_setOf_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
g : α → β
hf : TendstoUniformlyOn F f p s
hfg : EqOn f g s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), x ∈ s → (g x, F n x) ∈ u
[PROOFSTEP]
filter_upwards [hf u hu] with i hi a ha using hfg ha ▸ hi a ha
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
h : TendstoUniformlyOnFilter F f p p'
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p (comap g p')
[PROOFSTEP]
rw [tendstoUniformlyOnFilter_iff_tendsto] at h ⊢
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
h : Tendsto (fun q => (f q.snd, F q.fst q.snd)) (p ×ˢ p') (𝓤 β)
g : γ → α
⊢ Tendsto (fun q => ((f ∘ g) q.snd, (F q.fst ∘ g) q.snd)) (p ×ˢ comap g p') (𝓤 β)
[PROOFSTEP]
exact h.comp (tendsto_id.prod_map tendsto_comap)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
h : TendstoUniformlyOn F f p s
g : γ → α
⊢ TendstoUniformlyOn (fun n => F n ∘ g) (f ∘ g) p (g ⁻¹' s)
[PROOFSTEP]
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter] at h ⊢
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
h : TendstoUniformlyOnFilter F f p (𝓟 s)
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p (𝓟 (g ⁻¹' s))
[PROOFSTEP]
simpa [TendstoUniformlyOn, comap_principal] using TendstoUniformlyOnFilter.comp h g
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
h : TendstoUniformly F f p
g : γ → α
⊢ TendstoUniformly (fun n => F n ∘ g) (f ∘ g) p
[PROOFSTEP]
rw [tendstoUniformly_iff_tendstoUniformlyOnFilter] at h ⊢
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
h : TendstoUniformlyOnFilter F f p ⊤
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p ⊤
[PROOFSTEP]
simpa [principal_univ, comap_principal] using h.comp g
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : TendstoUniformlyOnFilter F f p p'
h' : TendstoUniformlyOnFilter F' f' q q'
⊢ TendstoUniformlyOnFilter (fun i => Prod.map (F i.fst) (F' i.snd)) (Prod.map f f') (p ×ˢ q) (p' ×ˢ q')
[PROOFSTEP]
rw [tendstoUniformlyOnFilter_iff_tendsto] at h h' ⊢
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : Tendsto (fun q => (f q.snd, F q.fst q.snd)) (p ×ˢ p') (𝓤 β)
h' : Tendsto (fun q => (f' q.snd, F' q.fst q.snd)) (q ×ˢ q') (𝓤 β')
⊢ Tendsto (fun q => (Prod.map f f' q.snd, Prod.map (F q.fst.fst) (F' q.fst.snd) q.snd)) ((p ×ˢ q) ×ˢ p' ×ˢ q')
    (𝓤 (β × β'))
[PROOFSTEP]
rw [uniformity_prod_eq_comap_prod, tendsto_comap_iff, ← map_swap4_prod, tendsto_map'_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : Tendsto (fun q => (f q.snd, F q.fst q.snd)) (p ×ˢ p') (𝓤 β)
h' : Tendsto (fun q => (f' q.snd, F' q.fst q.snd)) (q ×ˢ q') (𝓤 β')
⊢ Tendsto
    (((fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ∘ fun q =>
        (Prod.map f f' q.snd, Prod.map (F q.fst.fst) (F' q.fst.snd) q.snd)) ∘
      fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd))
    ((p ×ˢ p') ×ˢ q ×ˢ q') (𝓤 β ×ˢ 𝓤 β')
[PROOFSTEP]
convert h.prod_map h'
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s'✝ : Set α
x : α
p : Filter ι
p'✝ : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
s' : Set α'
h : TendstoUniformlyOn F f p s
h' : TendstoUniformlyOn F' f' p' s'
⊢ TendstoUniformlyOn (fun i => Prod.map (F i.fst) (F' i.snd)) (Prod.map f f') (p ×ˢ p') (s ×ˢ s')
[PROOFSTEP]
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter] at h h' ⊢
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s'✝ : Set α
x : α
p : Filter ι
p'✝ : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
s' : Set α'
h : TendstoUniformlyOnFilter F f p (𝓟 s)
h' : TendstoUniformlyOnFilter F' f' p' (𝓟 s')
⊢ TendstoUniformlyOnFilter (fun i => Prod.map (F i.fst) (F' i.snd)) (Prod.map f f') (p ×ˢ p') (𝓟 (s ×ˢ s'))
[PROOFSTEP]
simpa only [prod_principal_principal] using h.prod_map h'
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p'✝ : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
h : TendstoUniformly F f p
h' : TendstoUniformly F' f' p'
⊢ TendstoUniformly (fun i => Prod.map (F i.fst) (F' i.snd)) (Prod.map f f') (p ×ˢ p')
[PROOFSTEP]
rw [← tendstoUniformlyOn_univ, ← univ_prod_univ] at *
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p'✝ : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
h : TendstoUniformlyOn F f p univ
h' : TendstoUniformlyOn F' f' p' univ
⊢ TendstoUniformlyOn (fun i => Prod.map (F i.fst) (F' i.snd)) (Prod.map f f') (p ×ˢ p') (univ ×ˢ univ)
[PROOFSTEP]
exact h.prod_map h'
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
c : β
⊢ Tendsto (↿F) (p ×ˢ p') (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun x => c) p p'
[PROOFSTEP]
simp_rw [nhds_eq_comap_uniformity, tendsto_comap_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
c : β
⊢ Tendsto (Prod.mk c ∘ ↿F) (p ×ˢ p') (𝓤 β) ↔ TendstoUniformlyOnFilter F (fun x => c) p p'
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
c : β
⊢ Tendsto (↿F) (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOn F (fun x => c) p s
[PROOFSTEP]
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
c : β
⊢ Tendsto (↿F) (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun x => c) p (𝓟 s)
[PROOFSTEP]
exact tendsto_prod_filter_iff
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
c : β
⊢ Tendsto (↿F) (p ×ˢ ⊤) (𝓝 c) ↔ TendstoUniformly F (fun x => c) p
[PROOFSTEP]
rw [tendstoUniformly_iff_tendstoUniformlyOnFilter]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
c : β
⊢ Tendsto (↿F) (p ×ˢ ⊤) (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun x => c) p ⊤
[PROOFSTEP]
exact tendsto_prod_filter_iff
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
u : Set (β × β)
x✝ : u ∈ 𝓤 β
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), x ∈ ∅ → (f x, F n x) ∈ u
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ TendstoUniformlyOn F f p {x} ↔ Tendsto (fun n => F n x) p (𝓝 (f x))
[PROOFSTEP]
simp_rw [tendstoUniformlyOn_iff_tendsto, Uniform.tendsto_nhds_right, tendsto_def]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ (∀ (s : Set (β × β)), s ∈ 𝓤 β → (fun q => (f q.snd, F q.fst q.snd)) ⁻¹' s ∈ p ×ˢ 𝓟 {x}) ↔
    ∀ (s : Set (β × β)), s ∈ 𝓤 β → (fun x_1 => (f x, F x_1 x)) ⁻¹' s ∈ p
[PROOFSTEP]
exact forall₂_congr fun u _ => by simp [mem_prod_principal, preimage]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
u : Set (β × β)
x✝ : u ∈ 𝓤 β
⊢ (fun q => (f q.snd, F q.fst q.snd)) ⁻¹' u ∈ p ×ˢ 𝓟 {x} ↔ (fun x_1 => (f x, F x_1 x)) ⁻¹' u ∈ p
[PROOFSTEP]
simp [mem_prod_principal, preimage]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p'✝ : Filter α
g✝ : ι → α
g : ι → β
b : β
hg : Tendsto g p (𝓝 b)
p' : Filter α
⊢ TendstoUniformlyOnFilter (fun n x => g n) (fun x => b) p p'
[PROOFSTEP]
simpa only [nhds_eq_comap_uniformity, tendsto_comap_iff] using hg.comp (tendsto_fst (g := p'))
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
⊢ TendstoUniformlyOn F (F x) (𝓝[U] x) V
[PROOFSTEP]
set φ := fun q : α × β => ((x, q.2), q)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.snd), q)
⊢ TendstoUniformlyOn F (F x) (𝓝[U] x) V
[PROOFSTEP]
rw [tendstoUniformlyOn_iff_tendsto]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.snd), q)
⊢ Tendsto (fun q => (F x q.snd, F q.fst q.snd)) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
[PROOFSTEP]
change Tendsto (Prod.map (↿F) ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.snd), q)
⊢ Tendsto (Prod.map (↿F) ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
[PROOFSTEP]
simp only [nhdsWithin, SProd.sprod, Filter.prod, comap_inf, inf_assoc, comap_principal, inf_principal]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.snd), q)
⊢ Tendsto (Prod.map (↿F) ↿F ∘ fun q => ((x, q.snd), q)) (comap Prod.fst (𝓝 x) ⊓ 𝓟 (Prod.fst ⁻¹' U ∩ Prod.snd ⁻¹' V))
    (𝓤 γ)
[PROOFSTEP]
refine hF.comp (Tendsto.inf ?_ <| tendsto_principal_principal.2 <| fun x hx => ⟨⟨hU, hx.2⟩, hx⟩)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.snd), q)
⊢ Tendsto (fun q => ((x, q.snd), q)) (comap Prod.fst (𝓝 x)) (𝓤 (α × β))
[PROOFSTEP]
simp only [uniformity_prod_eq_comap_prod, tendsto_comap_iff, (· ∘ ·), nhds_eq_comap_uniformity, comap_comap]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.snd), q)
⊢ Tendsto (fun x_1 => ((x, x_1.fst), x_1.snd, x_1.snd)) (comap (fun x_1 => (x, x_1.fst)) (𝓤 α)) (𝓤 α ×ˢ 𝓤 β)
[PROOFSTEP]
exact tendsto_comap.prod_mk (tendsto_diag_uniformity _ _)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
hU : U ∈ 𝓝 x
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ univ)
⊢ TendstoUniformly F (F x) (𝓝 x)
[PROOFSTEP]
simpa only [tendstoUniformlyOn_univ, nhdsWithin_eq_nhds.2 hU] using hF.tendstoUniformlyOn (mem_of_mem_nhds hU)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f✝ : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
f : α → β → γ
h : UniformContinuous₂ f
x : α
⊢ UniformContinuousOn (↿f) (univ ×ˢ univ)
[PROOFSTEP]
rwa [univ_prod_univ, uniformContinuousOn_univ]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ UniformCauchySeqOn F p s ↔ UniformCauchySeqOnFilter F p (𝓟 s)
[PROOFSTEP]
simp only [UniformCauchySeqOn, UniformCauchySeqOnFilter]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
⊢ (∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ (x : α), x ∈ s → (F m.fst x, F m.snd x) ∈ u) ↔
    ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
[PROOFSTEP]
refine' forall₂_congr fun u hu => _
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ (∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ (x : α), x ∈ s → (F m.fst x, F m.snd x) ∈ u) ↔
    ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
[PROOFSTEP]
rw [eventually_prod_principal_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : UniformCauchySeqOn F p s
⊢ UniformCauchySeqOnFilter F p (𝓟 s)
[PROOFSTEP]
rwa [← uniformCauchySeqOn_iff_uniformCauchySeqOnFilter]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
⊢ UniformCauchySeqOnFilter F p p'
[PROOFSTEP]
intro u hu
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
[PROOFSTEP]
rcases comp_symm_of_uniformity hu with ⟨t, ht, htsymm, htmem⟩
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
⊢ ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
[PROOFSTEP]
have := tendsto_swap4_prod.eventually ((hF t ht).prod_mk (hF t ht))
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd) ∈
        t ∧
      (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd) ∈
        t
⊢ ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
[PROOFSTEP]
apply this.diag_of_prod_right.mono
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd) ∈
        t ∧
      (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd) ∈
        t
⊢ ∀ (x : (ι × ι) × α),
    (f
              (((x.fst, x.snd, x.snd).fst.fst, (x.fst, x.snd, x.snd).snd.fst), (x.fst, x.snd, x.snd).fst.snd,
                    (x.fst, x.snd, x.snd).snd.snd).fst.snd,
            F
              (((x.fst, x.snd, x.snd).fst.fst, (x.fst, x.snd, x.snd).snd.fst), (x.fst, x.snd, x.snd).fst.snd,
                    (x.fst, x.snd, x.snd).snd.snd).fst.fst
              (((x.fst, x.snd, x.snd).fst.fst, (x.fst, x.snd, x.snd).snd.fst), (x.fst, x.snd, x.snd).fst.snd,
                    (x.fst, x.snd, x.snd).snd.snd).fst.snd) ∈
          t ∧
        (f
              (((x.fst, x.snd, x.snd).fst.fst, (x.fst, x.snd, x.snd).snd.fst), (x.fst, x.snd, x.snd).fst.snd,
                    (x.fst, x.snd, x.snd).snd.snd).snd.snd,
            F
              (((x.fst, x.snd, x.snd).fst.fst, (x.fst, x.snd, x.snd).snd.fst), (x.fst, x.snd, x.snd).fst.snd,
                    (x.fst, x.snd, x.snd).snd.snd).snd.fst
              (((x.fst, x.snd, x.snd).fst.fst, (x.fst, x.snd, x.snd).snd.fst), (x.fst, x.snd, x.snd).fst.snd,
                    (x.fst, x.snd, x.snd).snd.snd).snd.snd) ∈
          t →
      (F x.fst.fst x.snd, F x.fst.snd x.snd) ∈ u
[PROOFSTEP]
simp only [and_imp, Prod.forall]
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd) ∈
        t ∧
      (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd) ∈
        t
⊢ ∀ (a b : ι) (b_1 : α), (f b_1, F a b_1) ∈ t → (f b_1, F b b_1) ∈ t → (F a b_1, F b b_1) ∈ u
[PROOFSTEP]
intro n1 n2 x hl hr
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd) ∈
        t ∧
      (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd) ∈
        t
n1 n2 : ι
x : α
hl : (f x, F n1 x) ∈ t
hr : (f x, F n2 x) ∈ t
⊢ (F n1 x, F n2 x) ∈ u
[PROOFSTEP]
exact Set.mem_of_mem_of_subset (prod_mk_mem_compRel (htsymm hl) hr) htmem
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
⊢ TendstoUniformlyOnFilter F f p p'
[PROOFSTEP]
intro u hu
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.snd, F n.fst n.snd) ∈ u
[PROOFSTEP]
rcases comp_symm_of_uniformity hu with
  ⟨t, ht, htsymm, htmem⟩
    -- We will choose n, x, and m simultaneously. n and x come from hF. m comes from hF'
      -- But we need to promote hF' to the full product filter to use it
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
⊢ ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.snd, F n.fst n.snd) ∈ u
[PROOFSTEP]
have hmc : ∀ᶠ x in (p ×ˢ p) ×ˢ p', Tendsto (fun n : ι => F n x.snd) p (𝓝 (f x.snd)) :=
  by
  rw [eventually_prod_iff]
  refine'
    ⟨fun _ => True, by simp, _, hF', by simp⟩
      -- To apply filter operations we'll need to do some order manipulation
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
⊢ ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
[PROOFSTEP]
rw [eventually_prod_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
⊢ ∃ pa,
    (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
      ∃ pb,
        (∀ᶠ (y : α) in p', pb y) ∧
          ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → Tendsto (fun n => F n (x, y).snd) p (𝓝 (f (x, y).snd))
[PROOFSTEP]
refine'
  ⟨fun _ => True, by simp, _, hF', by simp⟩
    -- To apply filter operations we'll need to do some order manipulation
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
⊢ ∀ᶠ (x : ι × ι) in p ×ˢ p, (fun x => True) x
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
⊢ ∀ {x : ι × ι},
    (fun x => True) x →
      ∀ {y : α}, Tendsto (fun n => F n y) p (𝓝 (f y)) → Tendsto (fun n => F n (x, y).snd) p (𝓝 (f (x, y).snd))
[PROOFSTEP]
simp
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
⊢ ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.snd, F n.fst n.snd) ∈ u
[PROOFSTEP]
rw [Filter.eventually_swap_iff]
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
⊢ ∀ᶠ (y : α × ι) in p' ×ˢ p, (f (Prod.swap y).snd, F (Prod.swap y).fst (Prod.swap y).snd) ∈ u
[PROOFSTEP]
have := tendsto_prodAssoc.eventually (tendsto_prod_swap.eventually ((hF t ht).and hmc))
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
⊢ ∀ᶠ (y : α × ι) in p' ×ˢ p, (f (Prod.swap y).snd, F (Prod.swap y).fst (Prod.swap y).snd) ∈ u
[PROOFSTEP]
apply this.curry.mono
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
⊢ ∀ (x : α × ι),
    (∀ᶠ (y : ι) in p,
        (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) (x, y))).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) (x, y))).snd,
              F (Prod.swap (↑(Equiv.prodAssoc α ι ι) (x, y))).fst.snd
                (Prod.swap (↑(Equiv.prodAssoc α ι ι) (x, y))).snd) ∈
            t ∧
          Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) (x, y))).snd) p
            (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) (x, y))).snd))) →
      (f (Prod.swap x).snd, F (Prod.swap x).fst (Prod.swap x).snd) ∈ u
[PROOFSTEP]
simp only [Equiv.prodAssoc_apply, eventually_and, eventually_const, Prod.snd_swap, Prod.fst_swap, and_imp, Prod.forall]
  -- Complete the proof
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
⊢ ∀ (a : α) (b : ι), (∀ᶠ (x : ι) in p, (F b a, F x a) ∈ t) → Tendsto (fun n => F n a) p (𝓝 (f a)) → (f a, F b a) ∈ u
[PROOFSTEP]
intro x n hx hm'
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun n => F n x) p (𝓝 (f x))
⊢ (f x, F n x) ∈ u
[PROOFSTEP]
refine' Set.mem_of_mem_of_subset (mem_compRel.mpr _) htmem
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun n => F n x) p (𝓝 (f x))
⊢ ∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t
[PROOFSTEP]
rw [Uniform.tendsto_nhds_right] at hm' 
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun x_1 => (f x, F x_1 x)) p (𝓤 β)
⊢ ∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t
[PROOFSTEP]
have := hx.and (hm' ht)
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this✝ :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun x_1 => (f x, F x_1 x)) p (𝓤 β)
this : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t ∧ (fun x_2 => (f x, F x_2 x)) x_1 ∈ t
⊢ ∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t
[PROOFSTEP]
obtain ⟨m, hm⟩ := this.exists
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : NeBot p
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.snd) p (𝓝 (f x.snd))
this✝ :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.fst (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd,
          F (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).fst.snd (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) ∈
        t ∧
      Tendsto (fun n => F n (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd) p
        (𝓝 (f (Prod.swap (↑(Equiv.prodAssoc α ι ι) x)).snd))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun x_1 => (f x, F x_1 x)) p (𝓤 β)
this : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t ∧ (fun x_2 => (f x, F x_2 x)) x_1 ∈ t
m : ι
hm : (F n x, F m x) ∈ t ∧ (fun x_1 => (f x, F x_1 x)) m ∈ t
⊢ ∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t
[PROOFSTEP]
exact ⟨F m x, ⟨hm.2, htsymm hm.1⟩⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
p'' : Filter ι
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p
⊢ UniformCauchySeqOnFilter F p'' p'
[PROOFSTEP]
intro u hu
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
p'' : Filter ι
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ᶠ (m : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
[PROOFSTEP]
have := (hf u hu).filter_mono (p'.prod_mono_left (Filter.prod_mono hp hp))
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
p'' : Filter ι
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p
u : Set (β × β)
hu : u ∈ 𝓤 β
this : ∀ᶠ (x : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F x.fst.fst x.snd, F x.fst.snd x.snd) ∈ u
⊢ ∀ᶠ (m : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
[PROOFSTEP]
exact this.mono (by simp)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
p'' : Filter ι
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p
u : Set (β × β)
hu : u ∈ 𝓤 β
this : ∀ᶠ (x : (ι × ι) × α) in (p'' ×ˢ p'') ×ˢ p', (F x.fst.fst x.snd, F x.fst.snd x.snd) ∈ u
⊢ ∀ (x : (ι × ι) × α), (F x.fst.fst x.snd, F x.fst.snd x.snd) ∈ u → (F x.fst.fst x.snd, F x.fst.snd x.snd) ∈ u
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
p'' : Filter α
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
this : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p'', (F x.fst.fst x.snd, F x.fst.snd x.snd) ∈ u
⊢ ∀ (x : (ι × ι) × α), (F x.fst.fst x.snd, F x.fst.snd x.snd) ∈ u → (F x.fst.fst x.snd, F x.fst.snd x.snd) ∈ u
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s'✝ : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
s' : Set α
hf : UniformCauchySeqOn F p s
hss' : s' ⊆ s
⊢ UniformCauchySeqOn F p s'
[PROOFSTEP]
rw [uniformCauchySeqOn_iff_uniformCauchySeqOnFilter] at hf ⊢
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s'✝ : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
s' : Set α
hf : UniformCauchySeqOnFilter F p (𝓟 s)
hss' : s' ⊆ s
⊢ UniformCauchySeqOnFilter F p (𝓟 s')
[PROOFSTEP]
exact hf.mono_right (le_principal_iff.mpr <| mem_principal.mpr hss')
[GOAL]
α : Type u
β : Type v
γ✝ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
γ : Type u_1
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ᶠ (m : (ι × ι) × γ) in (p ×ˢ p) ×ˢ comap g p',
    ((fun n => F n ∘ g) m.fst.fst m.snd, (fun n => F n ∘ g) m.fst.snd m.snd) ∈ u
[PROOFSTEP]
obtain ⟨pa, hpa, pb, hpb, hpapb⟩ := eventually_prod_iff.mp (hf u hu)
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ✝ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
γ : Type u_1
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).fst.fst (x, y).snd, F (x, y).fst.snd (x, y).snd) ∈ u
⊢ ∀ᶠ (m : (ι × ι) × γ) in (p ×ˢ p) ×ˢ comap g p',
    ((fun n => F n ∘ g) m.fst.fst m.snd, (fun n => F n ∘ g) m.fst.snd m.snd) ∈ u
[PROOFSTEP]
rw [eventually_prod_iff]
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ✝ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
γ : Type u_1
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).fst.fst (x, y).snd, F (x, y).fst.snd (x, y).snd) ∈ u
⊢ ∃ pa,
    (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
      ∃ pb,
        (∀ᶠ (y : γ) in comap g p', pb y) ∧
          ∀ {x : ι × ι},
            pa x →
              ∀ {y : γ},
                pb y → ((fun n => F n ∘ g) (x, y).fst.fst (x, y).snd, (fun n => F n ∘ g) (x, y).fst.snd (x, y).snd) ∈ u
[PROOFSTEP]
refine ⟨pa, hpa, pb ∘ g, ?_, fun hx _ hy => hpapb hx hy⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ✝ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
γ : Type u_1
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).fst.fst (x, y).snd, F (x, y).fst.snd (x, y).snd) ∈ u
⊢ ∀ᶠ (y : γ) in comap g p', (pb ∘ g) y
[PROOFSTEP]
exact eventually_comap.mpr (hpb.mono fun x hx y hy => by simp only [hx, hy, Function.comp_apply])
[GOAL]
α : Type u
β : Type v
γ✝ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g✝ : ι → α
γ : Type u_1
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).fst.fst (x, y).snd, F (x, y).fst.snd (x, y).snd) ∈ u
x : α
hx : pb x
y : γ
hy : g y = x
⊢ (pb ∘ g) y
[PROOFSTEP]
simp only [hx, hy, Function.comp_apply]
[GOAL]
α : Type u
β : Type v
γ✝ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
γ : Type u_1
hf : UniformCauchySeqOn F p s
g : γ → α
⊢ UniformCauchySeqOn (fun n => F n ∘ g) p (g ⁻¹' s)
[PROOFSTEP]
rw [uniformCauchySeqOn_iff_uniformCauchySeqOnFilter] at hf ⊢
[GOAL]
α : Type u
β : Type v
γ✝ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
γ : Type u_1
hf : UniformCauchySeqOnFilter F p (𝓟 s)
g : γ → α
⊢ UniformCauchySeqOnFilter (fun n => F n ∘ g) p (𝓟 (g ⁻¹' s))
[PROOFSTEP]
simpa only [UniformCauchySeqOn, comap_principal] using hf.comp g
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s'✝ : Set α
x : α
p : Filter ι
p'✝ : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
⊢ UniformCauchySeqOn (fun i => Prod.map (F i.fst) (F' i.snd)) (p ×ˢ p') (s ×ˢ s')
[PROOFSTEP]
intro u hu
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s'✝ : Set α
x : α
p : Filter ι
p'✝ : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
hu : u ∈ 𝓤 (β × β')
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ (x : α × α'),
      x ∈ s ×ˢ s' →
        ((fun i => Prod.map (F i.fst) (F' i.snd)) m.fst x, (fun i => Prod.map (F i.fst) (F' i.snd)) m.snd x) ∈ u
[PROOFSTEP]
rw [uniformity_prod_eq_prod, mem_map, mem_prod_iff] at hu 
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s'✝ : Set α
x : α
p : Filter ι
p'✝ : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
hu : ∃ t₁, t₁ ∈ 𝓤 β ∧ ∃ t₂, t₂ ∈ 𝓤 β' ∧ t₁ ×ˢ t₂ ⊆ (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹' u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ (x : α × α'),
      x ∈ s ×ˢ s' →
        ((fun i => Prod.map (F i.fst) (F' i.snd)) m.fst x, (fun i => Prod.map (F i.fst) (F' i.snd)) m.snd x) ∈ u
[PROOFSTEP]
obtain ⟨v, hv, w, hw, hvw⟩ := hu
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s'✝ : Set α
x : α
p : Filter ι
p'✝ : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : v ×ˢ w ⊆ (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹' u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ (x : α × α'),
      x ∈ s ×ˢ s' →
        ((fun i => Prod.map (F i.fst) (F' i.snd)) m.fst x, (fun i => Prod.map (F i.fst) (F' i.snd)) m.snd x) ∈ u
[PROOFSTEP]
simp_rw [mem_prod, Prod_map, and_imp, Prod.forall]
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s'✝ : Set α
x : α
p : Filter ι
p'✝ : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : v ×ˢ w ⊆ (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹' u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F m.fst.fst a, F' m.fst.snd b), F m.snd.fst a, F' m.snd.snd b) ∈ u
[PROOFSTEP]
rw [← Set.image_subset_iff] at hvw 
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s'✝ : Set α
x : α
p : Filter ι
p'✝ : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) '' v ×ˢ w ⊆ u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F m.fst.fst a, F' m.fst.snd b), F m.snd.fst a, F' m.snd.snd b) ∈ u
[PROOFSTEP]
apply (tendsto_swap4_prod.eventually ((h v hv).prod_mk (h' w hw))).mono
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s'✝ : Set α
x : α
p : Filter ι
p'✝ : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) '' v ×ˢ w ⊆ u
⊢ ∀ (x : (ι × ι') × ι × ι'),
    ((∀ (x_1 : α),
          x_1 ∈ s →
            (F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.fst x_1,
                F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd x_1) ∈
              v) ∧
        ∀ (x_1 : α'),
          x_1 ∈ s' →
            (F' ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.fst x_1,
                F' ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd x_1) ∈
              w) →
      ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F x.fst.fst a, F' x.fst.snd b), F x.snd.fst a, F' x.snd.snd b) ∈ u
[PROOFSTEP]
intro x hx a b ha hb
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s'✝ : Set α
x✝ : α
p : Filter ι
p'✝ : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) '' v ×ˢ w ⊆ u
x : (ι × ι') × ι × ι'
hx :
  (∀ (x_1 : α),
      x_1 ∈ s →
        (F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.fst x_1,
            F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd x_1) ∈
          v) ∧
    ∀ (x_1 : α'),
      x_1 ∈ s' →
        (F' ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.fst x_1,
            F' ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd x_1) ∈
          w
a : α
b : α'
ha : a ∈ s
hb : b ∈ s'
⊢ ((F x.fst.fst a, F' x.fst.snd b), F x.snd.fst a, F' x.snd.snd b) ∈ u
[PROOFSTEP]
refine' hvw ⟨_, mk_mem_prod (hx.1 a ha) (hx.2 b hb), rfl⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hp : NeBot p
hf : UniformCauchySeqOn F p s
hx : x ∈ s
⊢ Cauchy (map (fun i => F i x) p)
[PROOFSTEP]
simp only [cauchy_map_iff, hp, true_and_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hp : NeBot p
hf : UniformCauchySeqOn F p s
hx : x ∈ s
⊢ Tendsto (fun p => (F p.fst x, F p.snd x)) (p ×ˢ p) (𝓤 β)
[PROOFSTEP]
intro u hu
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hp : NeBot p
hf : UniformCauchySeqOn F p s
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ u ∈ map (fun p => (F p.fst x, F p.snd x)) (p ×ˢ p)
[PROOFSTEP]
rw [mem_map]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hp : NeBot p
hf : UniformCauchySeqOn F p s
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ (fun p => (F p.fst x, F p.snd x)) ⁻¹' u ∈ p ×ˢ p
[PROOFSTEP]
filter_upwards [hf u hu] with p hp using hp x hx
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s
⊢ TendstoUniformlyOn F f l s
[PROOFSTEP]
rw [tendstoUniformlyOn_iff_tendsto, tendsto_iff_seq_tendsto]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s
⊢ ∀ (x : ℕ → ι × α), Tendsto x atTop (l ×ˢ 𝓟 s) → Tendsto ((fun q => (f q.snd, F q.fst q.snd)) ∘ x) atTop (𝓤 β)
[PROOFSTEP]
intro u hu
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s
u : ℕ → ι × α
hu : Tendsto u atTop (l ×ˢ 𝓟 s)
⊢ Tendsto ((fun q => (f q.snd, F q.fst q.snd)) ∘ u) atTop (𝓤 β)
[PROOFSTEP]
rw [tendsto_prod_iff'] at hu 
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s
u : ℕ → ι × α
hu : Tendsto (fun n => (u n).fst) atTop l ∧ Tendsto (fun n => (u n).snd) atTop (𝓟 s)
⊢ Tendsto ((fun q => (f q.snd, F q.fst q.snd)) ∘ u) atTop (𝓤 β)
[PROOFSTEP]
specialize h (fun n => (u n).fst) hu.1
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
u : ℕ → ι × α
hu : Tendsto (fun n => (u n).fst) atTop l ∧ Tendsto (fun n => (u n).snd) atTop (𝓟 s)
h : TendstoUniformlyOn (fun n => F (u n).fst) f atTop s
⊢ Tendsto ((fun q => (f q.snd, F q.fst q.snd)) ∘ u) atTop (𝓤 β)
[PROOFSTEP]
rw [tendstoUniformlyOn_iff_tendsto] at h 
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
u : ℕ → ι × α
hu : Tendsto (fun n => (u n).fst) atTop l ∧ Tendsto (fun n => (u n).snd) atTop (𝓟 s)
h : Tendsto (fun q => (f q.snd, F (u q.fst).fst q.snd)) (atTop ×ˢ 𝓟 s) (𝓤 β)
⊢ Tendsto ((fun q => (f q.snd, F q.fst q.snd)) ∘ u) atTop (𝓤 β)
[PROOFSTEP]
exact h.comp (tendsto_id.prod_mk hu.2)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
h : TendstoUniformlyOn F f l s
u : ℕ → ι
hu : Tendsto u atTop l
⊢ TendstoUniformlyOn (fun n => F (u n)) f atTop s
[PROOFSTEP]
rw [tendstoUniformlyOn_iff_tendsto] at h ⊢
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
h : Tendsto (fun q => (f q.snd, F q.fst q.snd)) (l ×ˢ 𝓟 s) (𝓤 β)
u : ℕ → ι
hu : Tendsto u atTop l
⊢ Tendsto (fun q => (f q.snd, F (u q.fst) q.snd)) (atTop ×ˢ 𝓟 s) (𝓤 β)
[PROOFSTEP]
exact h.comp ((hu.comp tendsto_fst).prod_mk tendsto_snd)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
⊢ TendstoUniformly F f l ↔ ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformly (fun n => F (u n)) f atTop
[PROOFSTEP]
simp_rw [← tendstoUniformlyOn_univ]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
⊢ TendstoUniformlyOn F f l univ ↔ ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop univ
[PROOFSTEP]
exact tendstoUniformlyOn_iff_seq_tendstoUniformlyOn
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
⊢ TendstoLocallyUniformlyOn F f p univ ↔ TendstoLocallyUniformly F f p
[PROOFSTEP]
simp [TendstoLocallyUniformlyOn, TendstoLocallyUniformly, nhdsWithin_univ]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
x✝³ : α
x✝² : x✝³ ∈ s
x✝¹ : Set (β × β)
x✝ : x✝¹ ∈ 𝓤 β
⊢ (∃ t, t ∈ 𝓝[s] x✝³ ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ x✝¹) ↔
    x✝¹ ∈ map (fun y => (f y.snd, F y.fst y.snd)) (p ×ˢ 𝓝[s] x✝³)
[PROOFSTEP]
rw [mem_map, mem_prod_iff_right]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
x✝³ : α
x✝² : x✝³ ∈ s
x✝¹ : Set (β × β)
x✝ : x✝¹ ∈ 𝓤 β
⊢ (∃ t, t ∈ 𝓝[s] x✝³ ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ x✝¹) ↔
    ∃ t, t ∈ 𝓝[s] x✝³ ∧ ∀ᶠ (x : ι) in p, ∀ (y : α), y ∈ t → (x, y) ∈ (fun y => (f y.snd, F y.fst y.snd)) ⁻¹' x✝¹
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
hs : IsOpen s
x : α
hx : x ∈ s
⊢ Tendsto (fun y => (f y.snd, F y.fst y.snd)) (p ×ˢ 𝓝[s] x) (𝓤 β) ↔
    Tendsto (fun y => (f y.snd, F y.fst y.snd)) (p ×ˢ 𝓝 x) (𝓤 β)
[PROOFSTEP]
rw [hs.nhdsWithin_eq hx]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
⊢ TendstoLocallyUniformly F f p ↔ ∀ (x : α), Tendsto (fun y => (f y.snd, F y.fst y.snd)) (p ×ˢ 𝓝 x) (𝓤 β)
[PROOFSTEP]
simp [← tendstoLocallyUniformlyOn_univ, isOpen_univ.tendstoLocallyUniformlyOn_iff_forall_tendsto]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
⊢ TendstoLocallyUniformlyOn F f p s ↔ TendstoLocallyUniformly (fun i x => F i ↑x) (f ∘ Subtype.val) p
[PROOFSTEP]
simp only [tendstoLocallyUniformly_iff_forall_tendsto, Subtype.forall', tendsto_map'_iff,
  tendstoLocallyUniformlyOn_iff_forall_tendsto, ← map_nhds_subtype_val, prod_map_right]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
⊢ (∀ (x : { a // a ∈ s }), Tendsto ((fun y => (f y.snd, F y.fst y.snd)) ∘ Prod.map id Subtype.val) (p ×ˢ 𝓝 x) (𝓤 β)) ↔
    ∀ (x : ↑s), Tendsto (fun y => ((f ∘ Subtype.val) y.snd, F y.fst ↑y.snd)) (p ×ˢ 𝓝 x) (𝓤 β)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝¹ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : TendstoUniformlyOn F f p s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
x✝ : x ∈ s
⊢ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ s → (f y, F n y) ∈ u
[PROOFSTEP]
simpa using h u hu
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : TendstoUniformly F f p
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
⊢ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ univ → (f y, F n y) ∈ u
[PROOFSTEP]
simpa using h u hu
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
h' : s' ⊆ s
⊢ TendstoLocallyUniformlyOn F f p s'
[PROOFSTEP]
intro u hu x hx
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
h' : s' ⊆ s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s'
⊢ ∃ t, t ∈ 𝓝[s'] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
[PROOFSTEP]
rcases h u hu x (h' hx) with ⟨t, ht, H⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
h' : s' ⊆ s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s'
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ ∃ t, t ∈ 𝓝[s'] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
[PROOFSTEP]
exact ⟨t, nhdsWithin_mono x h' ht, H.mono fun n => id⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
S : Set (Set α)
hS : ∀ (s : Set α), s ∈ S → IsOpen s
h : ∀ (s : Set α), s ∈ S → TendstoLocallyUniformlyOn F f p s
⊢ TendstoLocallyUniformlyOn F f p (⋃₀ S)
[PROOFSTEP]
rw [sUnion_eq_biUnion]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
S : Set (Set α)
hS : ∀ (s : Set α), s ∈ S → IsOpen s
h : ∀ (s : Set α), s ∈ S → TendstoLocallyUniformlyOn F f p s
⊢ TendstoLocallyUniformlyOn F f p (⋃ (i : Set α) (_ : i ∈ S), i)
[PROOFSTEP]
exact tendstoLocallyUniformlyOn_biUnion hS h
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
hs₁ : IsOpen s₁
hs₂ : IsOpen s₂
h₁ : TendstoLocallyUniformlyOn F f p s₁
h₂ : TendstoLocallyUniformlyOn F f p s₂
⊢ TendstoLocallyUniformlyOn F f p (s₁ ∪ s₂)
[PROOFSTEP]
rw [← sUnion_pair]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
hs₁ : IsOpen s₁
hs₂ : IsOpen s₂
h₁ : TendstoLocallyUniformlyOn F f p s₁
h₂ : TendstoLocallyUniformlyOn F f p s₂
⊢ TendstoLocallyUniformlyOn F f p (⋃₀ {s₁, s₂})
[PROOFSTEP]
refine' tendstoLocallyUniformlyOn_sUnion _ _ _
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
hs₁ : IsOpen s₁
hs₂ : IsOpen s₂
h₁ : TendstoLocallyUniformlyOn F f p s₁
h₂ : TendstoLocallyUniformlyOn F f p s₂
⊢ ∀ (s : Set α), s ∈ {s₁, s₂} → IsOpen s
[PROOFSTEP]
simp [*]
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
hs₁ : IsOpen s₁
hs₂ : IsOpen s₂
h₁ : TendstoLocallyUniformlyOn F f p s₁
h₂ : TendstoLocallyUniformlyOn F f p s₂
⊢ ∀ (s : Set α), s ∈ {s₁, s₂} → TendstoLocallyUniformlyOn F f p s
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
⊢ TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p
[PROOFSTEP]
refine' ⟨fun h V hV => _, TendstoUniformly.tendstoLocallyUniformly⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
[PROOFSTEP]
choose U hU using h V hV
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
hU : ∀ (x : α), U x ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ U x → (f y, F n y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
[PROOFSTEP]
obtain ⟨t, ht⟩ := isCompact_univ.elim_nhds_subcover' (fun k _ => U k) fun k _ => (hU k).1
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
hU : ∀ (x : α), U x ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ U x → (f y, F n y) ∈ V
t : Finset ↑univ
ht : univ ⊆ ⋃ (x : ↑univ) (_ : x ∈ t), U ↑x
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
[PROOFSTEP]
replace hU := fun x : t => (hU x).2
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
ht : univ ⊆ ⋃ (x : ↑univ) (_ : x ∈ t), U ↑x
hU : ∀ (x : { x // x ∈ t }), ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ U ↑↑x → (f y, F n y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
[PROOFSTEP]
rw [← eventually_all] at hU 
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
ht : univ ⊆ ⋃ (x : ↑univ) (_ : x ∈ t), U ↑x
hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }) (y : α), y ∈ U ↑↑i → (f y, F x y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
[PROOFSTEP]
refine' hU.mono fun i hi x => _
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
ht : univ ⊆ ⋃ (x : ↑univ) (_ : x ∈ t), U ↑x
hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }) (y : α), y ∈ U ↑↑i → (f y, F x y) ∈ V
i : ι
hi : ∀ (i_1 : { x // x ∈ t }) (y : α), y ∈ U ↑↑i_1 → (f y, F i y) ∈ V
x : α
⊢ (f x, F i x) ∈ V
[PROOFSTEP]
specialize ht (mem_univ x)
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }) (y : α), y ∈ U ↑↑i → (f y, F x y) ∈ V
i : ι
hi : ∀ (i_1 : { x // x ∈ t }) (y : α), y ∈ U ↑↑i_1 → (f y, F i y) ∈ V
x : α
ht : x ∈ ⋃ (x : ↑univ) (_ : x ∈ t), U ↑x
⊢ (f x, F i x) ∈ V
[PROOFSTEP]
simp only [exists_prop, mem_iUnion, SetCoe.exists, exists_and_right, Subtype.coe_mk] at ht 
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }) (y : α), y ∈ U ↑↑i → (f y, F x y) ∈ V
i : ι
hi : ∀ (i_1 : { x // x ∈ t }) (y : α), y ∈ U ↑↑i_1 → (f y, F i y) ∈ V
x : α
ht : ∃ x_1, (∃ x, { val := x_1, property := (_ : x_1 ∈ univ) } ∈ t) ∧ x ∈ U x_1
⊢ (f x, F i x) ∈ V
[PROOFSTEP]
obtain ⟨y, ⟨hy₁, hy₂⟩, hy₃⟩ := ht
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }) (y : α), y ∈ U ↑↑i → (f y, F x y) ∈ V
i : ι
hi : ∀ (i_1 : { x // x ∈ t }) (y : α), y ∈ U ↑↑i_1 → (f y, F i y) ∈ V
x y : α
hy₃ : x ∈ U y
hy₁ : y ∈ univ
hy₂ : { val := y, property := (_ : y ∈ univ) } ∈ t
⊢ (f x, F i x) ∈ V
[PROOFSTEP]
exact hi ⟨⟨y, hy₁⟩, hy₂⟩ x hy₃
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
hs : IsCompact s
⊢ TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s
[PROOFSTEP]
haveI : CompactSpace s := isCompact_iff_compactSpace.mp hs
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
hs : IsCompact s
this : CompactSpace ↑s
⊢ TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s
[PROOFSTEP]
refine' ⟨fun h => _, TendstoUniformlyOn.tendstoLocallyUniformlyOn⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
hs : IsCompact s
this : CompactSpace ↑s
h : TendstoLocallyUniformlyOn F f p s
⊢ TendstoUniformlyOn F f p s
[PROOFSTEP]
rwa [tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe,
  tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace, ← tendstoUniformlyOn_iff_tendstoUniformly_comp_coe] at h 
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace γ
t : Set γ
h : TendstoLocallyUniformlyOn F f p s
g : γ → α
hg : MapsTo g t s
cg : ContinuousOn g t
⊢ TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p t
[PROOFSTEP]
intro u hu x hx
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace γ
t : Set γ
h : TendstoLocallyUniformlyOn F f p s
g : γ → α
hg : MapsTo g t s
cg : ContinuousOn g t
u : Set (β × β)
hu : u ∈ 𝓤 β
x : γ
hx : x ∈ t
⊢ ∃ t_1, t_1 ∈ 𝓝[t] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : γ), y ∈ t_1 → ((f ∘ g) y, (fun n => F n ∘ g) n y) ∈ u
[PROOFSTEP]
rcases h u hu (g x) (hg hx) with ⟨a, ha, H⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace γ
t : Set γ
h : TendstoLocallyUniformlyOn F f p s
g : γ → α
hg : MapsTo g t s
cg : ContinuousOn g t
u : Set (β × β)
hu : u ∈ 𝓤 β
x : γ
hx : x ∈ t
a : Set α
ha : a ∈ 𝓝[s] g x
H : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ a → (f y, F n y) ∈ u
⊢ ∃ t_1, t_1 ∈ 𝓝[t] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : γ), y ∈ t_1 → ((f ∘ g) y, (fun n => F n ∘ g) n y) ∈ u
[PROOFSTEP]
have : g ⁻¹' a ∈ 𝓝[t] x := (cg x hx).preimage_mem_nhdsWithin' (nhdsWithin_mono (g x) hg.image_subset ha)
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace γ
t : Set γ
h : TendstoLocallyUniformlyOn F f p s
g : γ → α
hg : MapsTo g t s
cg : ContinuousOn g t
u : Set (β × β)
hu : u ∈ 𝓤 β
x : γ
hx : x ∈ t
a : Set α
ha : a ∈ 𝓝[s] g x
H : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ a → (f y, F n y) ∈ u
this : g ⁻¹' a ∈ 𝓝[t] x
⊢ ∃ t_1, t_1 ∈ 𝓝[t] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : γ), y ∈ t_1 → ((f ∘ g) y, (fun n => F n ∘ g) n y) ∈ u
[PROOFSTEP]
exact ⟨g ⁻¹' a, this, H.mono fun n hn y hy => hn _ hy⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformly F f p
g : γ → α
cg : Continuous g
⊢ TendstoLocallyUniformly (fun n => F n ∘ g) (f ∘ g) p
[PROOFSTEP]
rw [← tendstoLocallyUniformlyOn_univ] at h ⊢
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformlyOn F f p univ
g : γ → α
cg : Continuous g
⊢ TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p univ
[PROOFSTEP]
rw [continuous_iff_continuousOn_univ] at cg 
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace γ
h : TendstoLocallyUniformlyOn F f p univ
g : γ → α
cg : ContinuousOn g univ
⊢ TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p univ
[PROOFSTEP]
exact h.comp _ (mapsTo_univ _ _) cg
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
⊢ List.TFAE
    [TendstoLocallyUniformlyOn G g p s, ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K,
      ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v]
[PROOFSTEP]
tfae_have 1 → 2
[GOAL]
case tfae_1_to_2
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
⊢ TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
[PROOFSTEP]
rintro h K hK1 hK2
[GOAL]
case tfae_1_to_2
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
h : TendstoLocallyUniformlyOn G g p s
K : Set α
hK1 : K ⊆ s
hK2 : IsCompact K
⊢ TendstoUniformlyOn G g p K
[PROOFSTEP]
exact (tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK2).mp (h.mono hK1)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
⊢ List.TFAE
    [TendstoLocallyUniformlyOn G g p s, ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K,
      ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v]
[PROOFSTEP]
tfae_have 2 → 3
[GOAL]
case tfae_2_to_3
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
⊢ (∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K) →
    ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
[PROOFSTEP]
rintro h x hx
[GOAL]
case tfae_2_to_3
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
h : ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
x : α
hx : x ∈ s
⊢ ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
[PROOFSTEP]
obtain ⟨K, ⟨hK1, hK2⟩, hK3⟩ := (compact_basis_nhds x).mem_iff.mp (hs.mem_nhds hx)
[GOAL]
case tfae_2_to_3.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
h : ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
x : α
hx : x ∈ s
K : Set α
hK3 : K ⊆ s
hK1 : K ∈ 𝓝 x
hK2 : IsCompact K
⊢ ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
[PROOFSTEP]
refine' ⟨K, nhdsWithin_le_nhds hK1, h K hK3 hK2⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 :
  (∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K) →
    ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
⊢ List.TFAE
    [TendstoLocallyUniformlyOn G g p s, ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K,
      ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v]
[PROOFSTEP]
tfae_have 3 → 1
[GOAL]
case tfae_3_to_1
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 :
  (∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K) →
    ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
⊢ (∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v) → TendstoLocallyUniformlyOn G g p s
[PROOFSTEP]
rintro h u hu x hx
[GOAL]
case tfae_3_to_1
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 :
  (∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K) →
    ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
h : ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (g y, G n y) ∈ u
[PROOFSTEP]
obtain ⟨v, hv1, hv2⟩ := h x hx
[GOAL]
case tfae_3_to_1.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 :
  (∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K) →
    ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
h : ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
v : Set α
hv1 : v ∈ 𝓝[s] x
hv2 : TendstoUniformlyOn G g p v
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (g y, G n y) ∈ u
[PROOFSTEP]
exact ⟨v, hv1, hv2 u hu⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 :
  (∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K) →
    ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
tfae_3_to_1 : (∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v) → TendstoLocallyUniformlyOn G g p s
⊢ List.TFAE
    [TendstoLocallyUniformlyOn G g p s, ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K,
      ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v]
[PROOFSTEP]
tfae_finish
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
⊢ TendstoLocallyUniformlyOn F f p s ↔ ∀ (x : α), x ∈ s → TendstoUniformlyOnFilter F f p (𝓝[s] x)
[PROOFSTEP]
simp only [TendstoUniformlyOnFilter, eventually_prod_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
⊢ TendstoLocallyUniformlyOn F f p s ↔
    ∀ (x : α),
      x ∈ s →
        ∀ (u : Set (β × β)),
          u ∈ 𝓤 β →
            ∃ pa,
              (∀ᶠ (x : ι) in p, pa x) ∧
                ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
⊢ TendstoLocallyUniformlyOn F f p s →
    ∀ (x : α),
      x ∈ s →
        ∀ (u : Set (β × β)),
          u ∈ 𝓤 β →
            ∃ pa,
              (∀ᶠ (x : ι) in p, pa x) ∧
                ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
[PROOFSTEP]
rintro h x hx u hu
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∃ pa,
    (∀ᶠ (x : ι) in p, pa x) ∧ ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
[PROOFSTEP]
obtain ⟨s, hs1, hs2⟩ := h u hu x hx
[GOAL]
case mp.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s✝ s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s✝
x : α
hx : x ∈ s✝
u : Set (β × β)
hu : u ∈ 𝓤 β
s : Set α
hs1 : s ∈ 𝓝[s✝] x
hs2 : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ s → (f y, F n y) ∈ u
⊢ ∃ pa,
    (∀ᶠ (x : ι) in p, pa x) ∧ ∃ pb, (∀ᶠ (y : α) in 𝓝[s✝] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
[PROOFSTEP]
exact ⟨_, hs2, _, eventually_of_mem hs1 fun x => id, fun hi y hy => hi y hy⟩
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
⊢ (∀ (x : α),
      x ∈ s →
        ∀ (u : Set (β × β)),
          u ∈ 𝓤 β →
            ∃ pa,
              (∀ᶠ (x : ι) in p, pa x) ∧
                ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u) →
    TendstoLocallyUniformlyOn F f p s
[PROOFSTEP]
rintro h u hu x hx
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h :
  ∀ (x : α),
    x ∈ s →
      ∀ (u : Set (β × β)),
        u ∈ 𝓤 β →
          ∃ pa,
            (∀ᶠ (x : ι) in p, pa x) ∧
              ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
[PROOFSTEP]
obtain ⟨pa, hpa, pb, hpb, h⟩ := h x hx u hu
[GOAL]
case mpr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h✝ :
  ∀ (x : α),
    x ∈ s →
      ∀ (u : Set (β × β)),
        u ∈ 𝓤 β →
          ∃ pa,
            (∀ᶠ (x : ι) in p, pa x) ∧
              ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
pa : ι → Prop
hpa : ∀ᶠ (x : ι) in p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in 𝓝[s] x, pb y
h : ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
[PROOFSTEP]
refine' ⟨pb, hpb, eventually_of_mem hpa fun i hi y hy => h hi hy⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
⊢ TendstoLocallyUniformly F f p ↔ ∀ (x : α), TendstoUniformlyOnFilter F f p (𝓝 x)
[PROOFSTEP]
simpa [← tendstoLocallyUniformlyOn_univ, ← nhdsWithin_univ] using
  @tendstoLocallyUniformlyOn_iff_filter _ _ _ _ F f univ p _
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
hf : TendstoLocallyUniformlyOn F f p s
a : α
ha : a ∈ s
⊢ Tendsto (fun i => F i a) p (𝓝 (f a))
[PROOFSTEP]
refine' ((tendstoLocallyUniformlyOn_iff_filter.mp hf) a ha).tendsto_at _
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
hf : TendstoLocallyUniformlyOn F f p s
a : α
ha : a ∈ s
⊢ 𝓟 {a} ≤ 𝓝[s] a
[PROOFSTEP]
simpa only [Filter.principal_singleton] using pure_le_nhdsWithin ha
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ (n : ι), EqOn (F n) (G n) s
⊢ TendstoLocallyUniformlyOn G f p s
[PROOFSTEP]
rintro u hu x hx
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ (n : ι), EqOn (F n) (G n) s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, G n y) ∈ u
[PROOFSTEP]
obtain ⟨t, ht, h⟩ := hf u hu x hx
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ (n : ι), EqOn (F n) (G n) s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝[s] x
h : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, G n y) ∈ u
[PROOFSTEP]
refine' ⟨s ∩ t, inter_mem self_mem_nhdsWithin ht, _⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ (n : ι), EqOn (F n) (G n) s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝[s] x
h : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ s ∩ t → (f y, G n y) ∈ u
[PROOFSTEP]
filter_upwards [h] with i hi y hy using hg i hy.1 ▸ hi y hy.2
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g✝ : ι → α
inst✝ : TopologicalSpace α
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : EqOn f g s
⊢ TendstoLocallyUniformlyOn F g p s
[PROOFSTEP]
rintro u hu x hx
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g✝ : ι → α
inst✝ : TopologicalSpace α
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : EqOn f g s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (g y, F n y) ∈ u
[PROOFSTEP]
obtain ⟨t, ht, h⟩ := hf u hu x hx
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g✝ : ι → α
inst✝ : TopologicalSpace α
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : EqOn f g s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝[s] x
h : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (g y, F n y) ∈ u
[PROOFSTEP]
refine' ⟨s ∩ t, inter_mem self_mem_nhdsWithin ht, _⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g✝ : ι → α
inst✝ : TopologicalSpace α
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : EqOn f g s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
t : Set α
ht : t ∈ 𝓝[s] x
h : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ s ∩ t → (g y, F n y) ∈ u
[PROOFSTEP]
filter_upwards [h] with i hi y hy using hg hy.1 ▸ hi y hy.2
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
hx : x ∈ s
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[s] x ∧ ∃ F, ContinuousWithinAt F s x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
⊢ ContinuousWithinAt f s x
[PROOFSTEP]
refine Uniform.continuousWithinAt_iff'_left.2 fun u₀ hu₀ => ?_
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
hx : x ∈ s
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[s] x ∧ ∃ F, ContinuousWithinAt F s x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
⊢ u₀ ∈ map (fun x_1 => (f x_1, f x)) (𝓝[s] x)
[PROOFSTEP]
obtain ⟨u₁, h₁, u₁₀⟩ : ∃ u ∈ 𝓤 β, u ○ u ⊆ u₀ := comp_mem_uniformity_sets hu₀
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
hx : x ∈ s
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[s] x ∧ ∃ F, ContinuousWithinAt F s x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
⊢ u₀ ∈ map (fun x_1 => (f x_1, f x)) (𝓝[s] x)
[PROOFSTEP]
obtain ⟨u₂, h₂, hsymm, u₂₁⟩ : ∃ u ∈ 𝓤 β, (∀ {a b}, (a, b) ∈ u → (b, a) ∈ u) ∧ u ○ u ⊆ u₁ := comp_symm_of_uniformity h₁
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
hx : x ∈ s
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[s] x ∧ ∃ F, ContinuousWithinAt F s x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
u₂ : Set (β × β)
h₂ : u₂ ∈ 𝓤 β
hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂
u₂₁ : u₂ ○ u₂ ⊆ u₁
⊢ u₀ ∈ map (fun x_1 => (f x_1, f x)) (𝓝[s] x)
[PROOFSTEP]
rcases L u₂ h₂ with ⟨t, tx, F, hFc, hF⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
hx : x ∈ s
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[s] x ∧ ∃ F, ContinuousWithinAt F s x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
u₂ : Set (β × β)
h₂ : u₂ ∈ 𝓤 β
hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂
u₂₁ : u₂ ○ u₂ ⊆ u₁
t : Set α
tx : t ∈ 𝓝[s] x
F : α → β
hFc : ContinuousWithinAt F s x
hF : ∀ (y : α), y ∈ t → (f y, F y) ∈ u₂
⊢ u₀ ∈ map (fun x_1 => (f x_1, f x)) (𝓝[s] x)
[PROOFSTEP]
have A : ∀ᶠ y in 𝓝[s] x, (f y, F y) ∈ u₂ := Eventually.mono tx hF
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
hx : x ∈ s
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[s] x ∧ ∃ F, ContinuousWithinAt F s x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
u₂ : Set (β × β)
h₂ : u₂ ∈ 𝓤 β
hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂
u₂₁ : u₂ ○ u₂ ⊆ u₁
t : Set α
tx : t ∈ 𝓝[s] x
F : α → β
hFc : ContinuousWithinAt F s x
hF : ∀ (y : α), y ∈ t → (f y, F y) ∈ u₂
A : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F y) ∈ u₂
⊢ u₀ ∈ map (fun x_1 => (f x_1, f x)) (𝓝[s] x)
[PROOFSTEP]
have B : ∀ᶠ y in 𝓝[s] x, (F y, F x) ∈ u₂ := Uniform.continuousWithinAt_iff'_left.1 hFc h₂
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
hx : x ∈ s
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[s] x ∧ ∃ F, ContinuousWithinAt F s x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
u₂ : Set (β × β)
h₂ : u₂ ∈ 𝓤 β
hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂
u₂₁ : u₂ ○ u₂ ⊆ u₁
t : Set α
tx : t ∈ 𝓝[s] x
F : α → β
hFc : ContinuousWithinAt F s x
hF : ∀ (y : α), y ∈ t → (f y, F y) ∈ u₂
A : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F y) ∈ u₂
B : ∀ᶠ (y : α) in 𝓝[s] x, (F y, F x) ∈ u₂
⊢ u₀ ∈ map (fun x_1 => (f x_1, f x)) (𝓝[s] x)
[PROOFSTEP]
have C : ∀ᶠ y in 𝓝[s] x, (f y, F x) ∈ u₁ := (A.and B).mono fun y hy => u₂₁ (prod_mk_mem_compRel hy.1 hy.2)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
hx : x ∈ s
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[s] x ∧ ∃ F, ContinuousWithinAt F s x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
u₂ : Set (β × β)
h₂ : u₂ ∈ 𝓤 β
hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂
u₂₁ : u₂ ○ u₂ ⊆ u₁
t : Set α
tx : t ∈ 𝓝[s] x
F : α → β
hFc : ContinuousWithinAt F s x
hF : ∀ (y : α), y ∈ t → (f y, F y) ∈ u₂
A : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F y) ∈ u₂
B : ∀ᶠ (y : α) in 𝓝[s] x, (F y, F x) ∈ u₂
C : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F x) ∈ u₁
⊢ u₀ ∈ map (fun x_1 => (f x_1, f x)) (𝓝[s] x)
[PROOFSTEP]
have : (F x, f x) ∈ u₁ := u₂₁ (prod_mk_mem_compRel (refl_mem_uniformity h₂) (hsymm (A.self_of_nhdsWithin hx)))
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
hx : x ∈ s
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[s] x ∧ ∃ F, ContinuousWithinAt F s x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
u₂ : Set (β × β)
h₂ : u₂ ∈ 𝓤 β
hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂
u₂₁ : u₂ ○ u₂ ⊆ u₁
t : Set α
tx : t ∈ 𝓝[s] x
F : α → β
hFc : ContinuousWithinAt F s x
hF : ∀ (y : α), y ∈ t → (f y, F y) ∈ u₂
A : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F y) ∈ u₂
B : ∀ᶠ (y : α) in 𝓝[s] x, (F y, F x) ∈ u₂
C : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F x) ∈ u₁
this : (F x, f x) ∈ u₁
⊢ u₀ ∈ map (fun x_1 => (f x_1, f x)) (𝓝[s] x)
[PROOFSTEP]
exact C.mono fun y hy => u₁₀ (prod_mk_mem_compRel hy this)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝 x ∧ ∃ F, ContinuousAt F x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
⊢ ContinuousAt f x
[PROOFSTEP]
rw [← continuousWithinAt_univ]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝 x ∧ ∃ F, ContinuousAt F x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
⊢ ContinuousWithinAt f univ x
[PROOFSTEP]
apply continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt (mem_univ _) _
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝 x ∧ ∃ F, ContinuousAt F x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
⊢ ∀ (u : Set (β × β)),
    u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[univ] x ∧ ∃ F, ContinuousWithinAt F univ x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
[PROOFSTEP]
simpa only [exists_prop, nhdsWithin_univ, continuousWithinAt_univ] using L
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ F, Continuous F ∧ ∀ (y : α), (f y, F y) ∈ u
⊢ ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ F, ContinuousOn F univ ∧ ∀ (y : α), y ∈ univ → (f y, F y) ∈ u
[PROOFSTEP]
simpa [continuous_iff_continuousOn_univ] using L
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s
inst✝ : NeBot p
⊢ ContinuousOn f s
[PROOFSTEP]
refine continuousOn_of_locally_uniform_approx_of_continuousWithinAt fun x hx u hu => ?_
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s
inst✝ : NeBot p
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∃ F, ContinuousWithinAt F s x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
[PROOFSTEP]
rcases h u hu x hx with ⟨t, ht, H⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s
inst✝ : NeBot p
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∃ F, ContinuousWithinAt F s x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
[PROOFSTEP]
rcases(hc.and H).exists with ⟨n, hFc, hF⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s
inst✝ : NeBot p
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
n : ι
hFc : ContinuousOn (F n) s
hF : ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∃ F, ContinuousWithinAt F s x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
[PROOFSTEP]
exact ⟨t, ht, ⟨F n, hFc.continuousWithinAt hx, hF⟩⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : ContinuousWithinAt f s x
hg : Tendsto g p (𝓝[s] x)
hunif : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ Tendsto (fun n => F n (g n)) p (𝓝 (f x))
[PROOFSTEP]
refine Uniform.tendsto_nhds_right.2 fun u₀ hu₀ => ?_
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : ContinuousWithinAt f s x
hg : Tendsto g p (𝓝[s] x)
hunif : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
⊢ u₀ ∈ map (fun x_1 => (f x, F x_1 (g x_1))) p
[PROOFSTEP]
obtain ⟨u₁, h₁, u₁₀⟩ : ∃ u ∈ 𝓤 β, u ○ u ⊆ u₀ := comp_mem_uniformity_sets hu₀
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : ContinuousWithinAt f s x
hg : Tendsto g p (𝓝[s] x)
hunif : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
⊢ u₀ ∈ map (fun x_1 => (f x, F x_1 (g x_1))) p
[PROOFSTEP]
rcases hunif u₁ h₁ with ⟨s, sx, hs⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s✝ s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : ContinuousWithinAt f s✝ x
hg : Tendsto g p (𝓝[s✝] x)
hunif : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[s✝] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), 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✝] x
hs : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ s → (f y, F n y) ∈ u₁
⊢ u₀ ∈ map (fun x_1 => (f x, F x_1 (g x_1))) p
[PROOFSTEP]
have A : ∀ᶠ n in p, g n ∈ s := hg sx
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s✝ s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : ContinuousWithinAt f s✝ x
hg : Tendsto g p (𝓝[s✝] x)
hunif : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[s✝] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), 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✝] x
hs : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ s → (f y, F n y) ∈ u₁
A : ∀ᶠ (n : ι) in p, g n ∈ s
⊢ u₀ ∈ map (fun x_1 => (f x, F x_1 (g x_1))) p
[PROOFSTEP]
have B : ∀ᶠ n in p, (f x, f (g n)) ∈ u₁ := hg (Uniform.continuousWithinAt_iff'_right.1 h h₁)
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s✝ s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : ContinuousWithinAt f s✝ x
hg : Tendsto g p (𝓝[s✝] x)
hunif : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[s✝] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), 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✝] x
hs : ∀ᶠ (n : ι) in p, ∀ (y : α), 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₁
⊢ u₀ ∈ map (fun x_1 => (f x, F x_1 (g x_1))) p
[PROOFSTEP]
exact B.mp <| A.mp <| hs.mono fun y H1 H2 H3 => u₁₀ (prod_mk_mem_compRel H3 (H1 _ H2))
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : ContinuousAt f x
hg : Tendsto g p (𝓝 x)
hunif : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ Tendsto (fun n => F n (g n)) p (𝓝 (f x))
[PROOFSTEP]
rw [← continuousWithinAt_univ] at h 
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝 x)
hunif : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ Tendsto (fun n => F n (g n)) p (𝓝 (f x))
[PROOFSTEP]
rw [← nhdsWithin_univ] at hunif hg 
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝[univ] x)
hunif : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[univ] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ Tendsto (fun n => F n (g n)) p (𝓝 (f x))
[PROOFSTEP]
exact tendsto_comp_of_locally_uniform_limit_within h hg hunif
