-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoLocallyUniformlyOn.comp [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

Proof state:
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
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 ∈ a, (f y, F n y) ∈ u
this : g ⁻¹' a ∈ 𝓝[t] x
⊢ ∃ t_1 ∈ 𝓝[t] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t_1, ((f ∘ g) y, (fun n => F n ∘ g) n y) ∈ u

Tactic:
exact ⟨g ⁻¹' a, this, H.mono fun n hn y hy => hn _ hy⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
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] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t_1, ((f ∘ g) y, (fun n => F n ∘ g) n y) ∈ u

Tactic:
rcases h u hu (g x) (hg hx) with ⟨a, ha, H⟩

Result:
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
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 ∈ a, (f y, F n y) ∈ u
⊢ ∃ t_1 ∈ 𝓝[t] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t_1, ((f ∘ g) y, (fun n => F n ∘ g) n y) ∈ u

Proof state:
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
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

Tactic:
intro u hu x hx

Result:
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
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] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t_1, ((f ∘ g) y, (fun n => F n ∘ g) n y) ∈ u

Proof state:
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
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 ∈ a, (f y, F n y) ∈ u
⊢ ∃ t_1 ∈ 𝓝[t] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t_1, ((f ∘ g) y, (fun n => F n ∘ g) n y) ∈ u

Tactic:
have : g ⁻¹' a ∈ 𝓝[t] x :=
  (cg x hx).preimage_mem_nhdsWithin' (nhdsWithin_mono (g x) hg.image_subset ha)

Result:
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
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 ∈ a, (f y, F n y) ∈ u
this : g ⁻¹' a ∈ 𝓝[t] x
⊢ ∃ t_1 ∈ 𝓝[t] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t_1, ((f ∘ g) y, (fun n => F n ∘ g) n y) ∈ u