-- 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:
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

Tactic:
have h' : TendstoUniformly F' f p := by
  rwa [tendstoUniformly_congr hF] 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 : α → β
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

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
⊢ ∃ s ∈ p, EqOn F F' s

Tactic:
refine ⟨s', hs', fun y hy => by aesop⟩

Result:
no goals

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 : ι) (x : α), F' i x ∈ s

Tactic:
aesop

Result:
no goals

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
⊢ F =ᶠ[p] F'

Tactic:
rw [eventuallyEq_iff_exists_mem]

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
⊢ ∃ s ∈ p, EqOn F F' s

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 : ι) 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 x => g (F i x)) (fun x => g (f x)) p

Tactic:
classical
rw [eventually_iff_exists_mem] at hF
obtain ⟨s', hs', hs⟩ := hF
let F' : ι → α → β := fun (i : ι) x => if i ∈ s' then F i x else f x
have hF : F =ᶠ[p] F' :=  by
  rw [eventuallyEq_iff_exists_mem]
  refine ⟨s', hs', fun y hy => by aesop⟩
have h' : TendstoUniformly F' f p := by
  rwa [tendstoUniformly_congr hF] at h
apply (tendstoUniformly_congr _).mpr
  (UniformContinuousOn.comp_tendstoUniformly s F' f (by aesop) hf hg h')
rw [eventuallyEq_iff_exists_mem]
refine ⟨s', hs', fun i hi => by 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
⊢ TendstoUniformly (fun i x => g (F i x)) (fun x => g (f x)) p

Tactic:
let F' : ι → α → β := fun (i : ι) x => if i ∈ s' then F i x else f x

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
⊢ 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 : ∀ (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
y : ι
hy : y ∈ s'
⊢ F y = F' y

Tactic:
aesop

Result:
no goals

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
⊢ ∃ s ∈ p, EqOn (fun i x => g (F i x)) (fun i x => g (F' i x)) s

Tactic:
refine ⟨s', hs', fun i hi => by aesop⟩

Result:
no goals

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 : ι) 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 x => g (F i x)) (fun x => g (f x)) p

Tactic:
rw [eventually_iff_exists_mem] at hF

Result:
α : 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

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
⊢ (fun i x => g (F i x)) =ᶠ[p] fun i x => g (F' i x)

Tactic:
rw [eventuallyEq_iff_exists_mem]

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
⊢ ∃ s ∈ p, EqOn (fun i x => g (F i x)) (fun i x => g (F' i x)) s