obtain ⟨i, l4, l5, l6⟩ := (l1.and (l2.and l3)).exists
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
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