-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoLocallyUniformlyOn.continuousOn (h : TendstoLocallyUniformlyOn F f p s)
    (hc : ∀ᶠ n in p, ContinuousOn (F n) s) [NeBot p] : ContinuousOn f s

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝¹ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s
inst✝ : p.NeBot
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u

Tactic:
rcases h u hu x hx with ⟨t, ht, H⟩

Result:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝¹ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s
inst✝ : p.NeBot
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝¹ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s
inst✝ : p.NeBot
⊢ ContinuousOn f s

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

Result:
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝¹ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s
inst✝ : p.NeBot
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u

Proof state:
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝¹ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s
inst✝ : p.NeBot
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
n : ι
hFc : ContinuousOn (F n) s
hF : ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u

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

Result:
no goals

Proof state:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝¹ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s
inst✝ : p.NeBot
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u

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

Result:
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝¹ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s
inst✝ : p.NeBot
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
n : ι
hFc : ContinuousOn (F n) s
hF : ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u