-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto
    (h1 : TendstoUniformlyOnFilter F f p p') (h2 : ∀ᶠ i in p, Tendsto (F i) p' (𝓝 (L i)))
    (h3 : Tendsto L p (𝓝 ℓ)) : Tendsto f p' (𝓝 ℓ)

Proof state:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Tactic:
have p1 : ∀ᶠ i in p, (L i, ℓ) ∈ t := tendsto_nhds_left.mp h3 ht

Result:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
⊢ Tendsto (fun x => (f x, ℓ)) p' (𝓤 β)

Tactic:
intro s hs

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
⊢ s ∈ map (fun x => (f x, ℓ)) p'

Proof state:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Tactic:
have p2 : ∀ᶠ i in p, ∀ᶠ x in p', (F i x, L i) ∈ t := by
  filter_upwards [h2] with i h2 using tendsto_nhds_left.mp h2 ht

Result:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
p2 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
⊢ Tendsto f p' (𝓝 ℓ)

Tactic:
rw [tendsto_nhds_left]

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
⊢ Tendsto (fun x => (f x, ℓ)) p' (𝓤 β)

Proof state:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
p2 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
p3 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (f x, F i x) ∈ t
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Tactic:
obtain ⟨i, p4, p5, p6⟩ := (p1.and (p2.and p3)).exists

Result:
case intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
p2 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
p3 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (f x, F i x) ∈ t
i : ι
p4 : (L i, ℓ) ∈ t
p5 : ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
p6 : ∀ᶠ (x : α) in p', (f x, F i x) ∈ t
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Proof state:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
p2 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Tactic:
have p3 : ∀ᶠ i in p, ∀ᶠ x in p', (f x, F i x) ∈ t := (h1 t ht).curry

Result:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
p2 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
p3 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (f x, F i x) ∈ t
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
⊢ s ∈ map (fun x => (f x, ℓ)) p'

Tactic:
rw [mem_map, Set.preimage, ← eventually_iff]

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
⊢ ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t

Tactic:
filter_upwards [h2] with i h2 using tendsto_nhds_left.mp h2 ht

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Tactic:
obtain ⟨t, ht, hts⟩ := comp3_mem_uniformity hs

Result:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s