Theorem: TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto (PrimeNumberTheoremAnd/Mathlib/Topology/UniformSpace/UniformConvergence.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
⊢ Tendsto f p (𝓝 ℓ)
Tactic:
rw [tendsto_nhds_left]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
⊢ Tendsto (fun x => (f x, ℓ)) p (𝓤 β)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
⊢ Tendsto (fun x => (f x, ℓ)) p (𝓤 β)
Tactic:
intro s hs
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
⊢ s ∈ map (fun x => (f x, ℓ)) p

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
⊢ s ∈ map (fun x => (f x, ℓ)) p
Tactic:
change ∀ᶠ x in p, (f x, ℓ) ∈ s
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s
Tactic:
obtain ⟨t, ht, hts⟩ := comp3_mem_uniformity hs
State after:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s

State before:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s
Tactic:
have l1 : ∀ᶠ i in l, (L i, ℓ) ∈ t := tendsto_nhds_left.mp h3 ht
State after:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
l1 : ∀ᶠ (i : ι) in l, (L i, ℓ) ∈ t
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s

State before:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
l1 : ∀ᶠ (i : ι) in l, (L i, ℓ) ∈ t
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s
Tactic:
have l2 : ∀ᶠ i in l, ∀ᶠ x in p, (F i x, L i) ∈ t := by
  filter_upwards [h2] with i h2 using tendsto_nhds_left.mp h2 ht
State after:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
l1 : ∀ᶠ (i : ι) in l, (L i, ℓ) ∈ t
l2 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (F i x, L i) ∈ t
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s

State before:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
l1 : ∀ᶠ (i : ι) in l, (L i, ℓ) ∈ t
l2 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (F i x, L i) ∈ t
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s
Tactic:
have l3 : ∀ᶠ i in l, ∀ᶠ x in p, (f x, F i x) ∈ t := (h1 t ht).curry
State after:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
l1 : ∀ᶠ (i : ι) in l, (L i, ℓ) ∈ t
l2 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (F i x, L i) ∈ t
l3 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (f x, F i x) ∈ t
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s

State before:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
l1 : ∀ᶠ (i : ι) in l, (L i, ℓ) ∈ t
l2 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (F i x, L i) ∈ t
l3 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (f x, F i x) ∈ t
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s
Tactic:
obtain ⟨i, l4, l5, l6⟩ := (l1.and (l2.and l3)).exists
State after:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
l1 : ∀ᶠ (i : ι) in l, (L i, ℓ) ∈ t
l2 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (F i x, L i) ∈ t
l3 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (f x, F i x) ∈ t
i : ι
l4 : (L i, ℓ) ∈ t
l5 : ∀ᶠ (x : α) in p, (F i x, L i) ∈ t
l6 : ∀ᶠ (x : α) in p, (f x, F i x) ∈ t
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s

State before:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
l1 : ∀ᶠ (i : ι) in l, (L i, ℓ) ∈ t
l2 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (F i x, L i) ∈ t
l3 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (f x, F i x) ∈ t
i : ι
l4 : (L i, ℓ) ∈ t
l5 : ∀ᶠ (x : α) in p, (F i x, L i) ∈ t
l6 : ∀ᶠ (x : α) in p, (f x, F i x) ∈ t
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s
Tactic:
filter_upwards [l5, l6] with x l5 l6 using hts ⟨F i x, l6, L i, l5, l4⟩
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
l1 : ∀ᶠ (i : ι) in l, (L i, ℓ) ∈ t
⊢ ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (F i x, L i) ∈ t
Tactic:
filter_upwards [h2] with i h2 using tendsto_nhds_left.mp h2 ht
State after:
no goals