-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem UniformContinuousOn.comp_tendstoUniformly (s : Set β) (F : ι → α → β) (f : α → β)
    (hF : ∀ i x, F i x ∈ s) (hf : ∀ x, f x ∈ s)
    {g : β → γ} (hg : UniformContinuousOn g s) (h : TendstoUniformly F f p) :
    TendstoUniformly (fun i x => g (F i x)) (fun x => g (f x)) p

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.restrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 => ↑(F' i i_1)) = F
h✝¹ : TendstoUniformly (fun i i_1 => ↑(F' i i_1)) f p
f' : α → ↑s
hf' : (fun i => ↑(f' i)) = f
h✝ h : TendstoUniformly (fun i i_1 => ↑(F' i i_1)) (fun i => ↑(f' i)) p
⊢ TendstoUniformly (fun i x => g ↑(F' i x)) (fun x => g ↑(f' x)) p

Tactic:
rw [tendstoUniformly_iff_tendsto] at h

Result:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.restrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 => ↑(F' i i_1)) = F
h✝¹ : TendstoUniformly (fun i i_1 => ↑(F' i i_1)) f p
f' : α → ↑s
hf' : (fun i => ↑(f' i)) = f
h✝ : TendstoUniformly (fun i i_1 => ↑(F' i i_1)) (fun i => ↑(f' i)) p
h : Tendsto (fun q => (↑(f' q.2), ↑(F' q.1 q.2))) (p ×ˢ ⊤) (𝓤 β)
⊢ TendstoUniformly (fun i x => g ↑(F' i x)) (fun x => g ↑(f' x)) p

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
hF : ∀ (i : ι) (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
g : β → γ
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
⊢ TendstoUniformly (fun i x => g (F i x)) (fun x => g (f x)) p

Tactic:
rw [uniformContinuousOn_iff_restrict] at hg

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
hF : ∀ (i : ι) (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
g : β → γ
hg : UniformContinuous (s.restrict g)
h : TendstoUniformly F f p
⊢ TendstoUniformly (fun i x => g (F i x)) (fun x => g (f x)) p

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
hF : ∀ (i : ι) (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
g : β → γ
hg : UniformContinuous (s.restrict g)
h : TendstoUniformly F f p
⊢ TendstoUniformly (fun i x => g (F i x)) (fun x => g (f x)) p

Tactic:
lift F to ι → α → s using hF with F' hF'

Result:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
hf : ∀ (x : α), f x ∈ s
g : β → γ
hg : UniformContinuous (s.restrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 => ↑(F' i i_1)) = F
h✝ h : TendstoUniformly (fun i i_1 => ↑(F' i i_1)) f p
⊢ TendstoUniformly (fun i x => g ↑(F' i x)) (fun x => g (f x)) p

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.restrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 => ↑(F' i i_1)) = F
h✝¹ : TendstoUniformly (fun i i_1 => ↑(F' i i_1)) f p
f' : α → ↑s
hf' : (fun i => ↑(f' i)) = f
h✝ : TendstoUniformly (fun i i_1 => ↑(F' i i_1)) (fun i => ↑(f' i)) p
h : Tendsto (fun q => (↑(f' q.2), ↑(F' q.1 q.2))) (p ×ˢ ⊤) (𝓤 β)
⊢ TendstoUniformly (fun i x => g ↑(F' i x)) (fun x => g ↑(f' x)) p

Tactic:
have : Tendsto (fun q : ι × α ↦ (f' q.2, (F' q.1 q.2))) (p ×ˢ ⊤) (𝓤 s) :=
  h.of_tendsto_comp isUniformEmbedding_subtype_val.comap_uniformity.le

Result:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.restrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 => ↑(F' i i_1)) = F
h✝¹ : TendstoUniformly (fun i i_1 => ↑(F' i i_1)) f p
f' : α → ↑s
hf' : (fun i => ↑(f' i)) = f
h✝ : TendstoUniformly (fun i i_1 => ↑(F' i i_1)) (fun i => ↑(f' i)) p
h : Tendsto (fun q => (↑(f' q.2), ↑(F' q.1 q.2))) (p ×ˢ ⊤) (𝓤 β)
this : Tendsto (fun q => (f' q.2, F' q.1 q.2)) (p ×ˢ ⊤) (𝓤 ↑s)
⊢ TendstoUniformly (fun i x => g ↑(F' i x)) (fun x => g ↑(f' x)) p

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.restrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 => ↑(F' i i_1)) = F
h✝¹ : TendstoUniformly (fun i i_1 => ↑(F' i i_1)) f p
f' : α → ↑s
hf' : (fun i => ↑(f' i)) = f
h✝ : TendstoUniformly (fun i i_1 => ↑(F' i i_1)) (fun i => ↑(f' i)) p
h : Tendsto (fun q => (↑(f' q.2), ↑(F' q.1 q.2))) (p ×ˢ ⊤) (𝓤 β)
this : Tendsto (fun q => (f' q.2, F' q.1 q.2)) (p ×ˢ ⊤) (𝓤 ↑s)
⊢ TendstoUniformly (fun i x => g ↑(F' i x)) (fun x => g ↑(f' x)) p

Tactic:
apply UniformContinuous.comp_tendstoUniformly hg ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.restrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 => ↑(F' i i_1)) = F
h✝¹ : TendstoUniformly (fun i i_1 => ↑(F' i i_1)) f p
f' : α → ↑s
hf' : (fun i => ↑(f' i)) = f
h✝ : TendstoUniformly (fun i i_1 => ↑(F' i i_1)) (fun i => ↑(f' i)) p
h : Tendsto (fun q => (↑(f' q.2), ↑(F' q.1 q.2))) (p ×ˢ ⊤) (𝓤 β)
this : Tendsto (fun q => (f' q.2, F' q.1 q.2)) (p ×ˢ ⊤) (𝓤 ↑s)
⊢ TendstoUniformly F' f' p

Proof state:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
hf : ∀ (x : α), f x ∈ s
g : β → γ
hg : UniformContinuous (s.restrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 => ↑(F' i i_1)) = F
h✝ h : TendstoUniformly (fun i i_1 => ↑(F' i i_1)) f p
⊢ TendstoUniformly (fun i x => g ↑(F' i x)) (fun x => g (f x)) p

Tactic:
lift f to α → s using hf with f' hf'

Result:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.restrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 => ↑(F' i i_1)) = F
h✝¹ : TendstoUniformly (fun i i_1 => ↑(F' i i_1)) f p
f' : α → ↑s
hf' : (fun i => ↑(f' i)) = f
h✝ h : TendstoUniformly (fun i i_1 => ↑(F' i i_1)) (fun i => ↑(f' i)) p
⊢ TendstoUniformly (fun i x => g ↑(F' i x)) (fun x => g ↑(f' x)) p

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.restrict g)
F' : ι → α → ↑s
hF' : (fun i i_1 => ↑(F' i i_1)) = F
h✝¹ : TendstoUniformly (fun i i_1 => ↑(F' i i_1)) f p
f' : α → ↑s
hf' : (fun i => ↑(f' i)) = f
h✝ : TendstoUniformly (fun i i_1 => ↑(F' i i_1)) (fun i => ↑(f' i)) p
h : Tendsto (fun q => (↑(f' q.2), ↑(F' q.1 q.2))) (p ×ˢ ⊤) (𝓤 β)
this : Tendsto (fun q => (f' q.2, F' q.1 q.2)) (p ×ˢ ⊤) (𝓤 ↑s)
⊢ TendstoUniformly F' f' p

Tactic:
rwa [← tendstoUniformly_iff_tendsto] at this

Result:
no goals