-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem UniformContinuousOn.comp_tendstoUniformly_eventually (s : Set β) (F : ι → α → β) (f : α → β)
    (hF : ∀ᶠ i in p, ∀ x, F i x ∈ s) (hf : ∀ x, f x ∈ s)
    {g : β → γ} (hg : UniformContinuousOn g s) (h : TendstoUniformly F f p) :
    TendstoUniformly (fun i => fun 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 : ∀ (x : α), f x ∈ s
g : β → γ
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x => if i ∈ s' then F i x else f x
hF : F =ᶠ[p] F'
h' : TendstoUniformly F' f p
i : ι
hi : i ∈ s'
⊢ (fun i x => g (F i x)) i = (fun i x => g (F' i x)) i

Tactic:
aesop

Result:
no goals

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 : α → β
hf : ∀ (x : α), f x ∈ s
g : β → γ
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x => if i ∈ s' then F i x else f x
hF : F =ᶠ[p] F'
h' : TendstoUniformly F' f p
⊢ TendstoUniformly (fun i x => g (F i x)) (fun x => g (f x)) p

Tactic:
apply (tendstoUniformly_congr _).mpr
  (UniformContinuousOn.comp_tendstoUniformly s F' f (by aesop) hf hg h')

Result:
α : 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 : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x => if i ∈ s' then F i x else f x
hF : F =ᶠ[p] F'
h' : TendstoUniformly F' f p
⊢ (fun i x => g (F i x)) =ᶠ[p] fun i x => g (F' i x)

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 : ∀ (x : α), f x ∈ s
g : β → γ
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x => if i ∈ s' then F i x else f x
hF : F =ᶠ[p] F'
⊢ TendstoUniformly F' f p

Tactic:
rwa [tendstoUniformly_congr hF] at h

Result:
no goals

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 : α → β
hf : ∀ (x : α), f x ∈ s
g : β → γ
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x => if i ∈ s' then F i x else f x
⊢ TendstoUniformly (fun i x => g (F i x)) (fun x => g (f x)) p

Tactic:
have hF : F =ᶠ[p] F' :=  by
  rw [eventuallyEq_iff_exists_mem]
  refine ⟨s', hs', fun y hy => by aesop⟩

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 : α → β
hf : ∀ (x : α), f x ∈ s
g : β → γ
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x => if i ∈ s' then F i x else f x
hF : F =ᶠ[p] F'
⊢ 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 : ∃ v ∈ p, ∀ y ∈ v, ∀ (x : α), F y 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:
obtain ⟨s', hs', hs⟩ := 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 : α → β
hf : ∀ (x : α), f x ∈ s
g : β → γ
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
⊢ TendstoUniformly (fun i x => g (F i x)) (fun x => g (f x)) p