awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuous (s.restrict (π := fun (a : β) ↦ γ) g)
F' : (i : ι) → α → (↑s : Type u_2)
hF' : (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) = F
comp_tendstoUniformly :
  ∀ (hF : ∀ (i : ι) (x : α), (↑(F' i x) : β) ∈ s) (hf : ∀ (x : α), f x ∈ s) (hg : UniformContinuousOn g s)
    (h : TendstoUniformly (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) f p),
    TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (f x)) p
h : TendstoUniformly (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) f p
lift :
  ∀ (f' : (i : α) → (↑s : Type u_2)) (hf' : (fun (i : α) ↦ (↑(f' i) : β)) = f)
    (comp_tendstoUniformly :
      ∀ (hF : ∀ (i : ι) (x : α), (↑(F' i x) : β) ∈ s) (hf : ∀ (x : α), (↑(f' x) : β) ∈ s) (hg : UniformContinuousOn g s)
        (h :
          TendstoUniformly.{u_1, u_2, u_4} (β := β) (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β))
            (fun (i : α) ↦ (↑(f' i) : β)) p),
        TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β))
          (fun (x : α) ↦ g (↑(f' x) : β)) p)
    (h :
      TendstoUniformly.{u_1, u_2, u_4} (β := β) (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β))
        (fun (i : α) ↦ (↑(f' i) : β)) p),
    TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (↑(f' x) : β))
      p
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (f x)) p

Tactic:
lift f to α → s using hf with f' hf'
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.restrict (π := fun (a : β) ↦ γ) g)
F' : (i : ι) → α → (↑s : Type u_2)
hF' : (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) = F
f' : (i : α) → (↑s : Type u_2)
hf' : (fun (i : α) ↦ (↑(f' i) : β)) = f
comp_tendstoUniformly :
  ∀ (hF : ∀ (i : ι) (x : α), (↑(F' i x) : β) ∈ s) (hf : ∀ (x : α), (↑(f' x) : β) ∈ s) (hg : UniformContinuousOn g s)
    (h :
      TendstoUniformly.{u_1, u_2, u_4} (β := β) (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β))
        (fun (i : α) ↦ (↑(f' i) : β)) p),
    TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (↑(f' x) : β))
      p
h :
  TendstoUniformly.{u_1, u_2, u_4} (β := β) (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) (fun (i : α) ↦ (↑(f' i) : β)) p
⊢ Tendsto (fun (q : ι × α) ↦ ((↑(f' q.2) : β), (↑(F' q.1 q.2) : β))) (SProd.sprod (β := Filter α) p ⊤) (𝓤 β)

Tactic:
rw [tendstoUniformly_iff_tendsto] at h

Premises used: tendstoUniformly_iff_tendsto
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.restrict (π := fun (a : β) ↦ γ) g)
F' : (i : ι) → α → (↑s : Type u_2)
hF' : (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) = F
f' : (i : α) → (↑s : Type u_2)
hf' : (fun (i : α) ↦ (↑(f' i) : β)) = f
comp_tendstoUniformly :
  ∀ (hF : ∀ (i : ι) (x : α), (↑(F' i x) : β) ∈ s) (hf : ∀ (x : α), (↑(f' x) : β) ∈ s) (hg : UniformContinuousOn g s)
    (h :
      TendstoUniformly.{u_1, u_2, u_4} (β := β) (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β))
        (fun (i : α) ↦ (↑(f' i) : β)) p),
    TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (↑(f' x) : β))
      p
h : Tendsto (fun (q : ι × α) ↦ ((↑(f' q.2) : β), (↑(F' q.1 q.2) : β))) (SProd.sprod (β := Filter α) p ⊤) (𝓤 β)
⊢ Tendsto (β := (↑s : Type u_2) × (↑s : Type u_2)) (fun (q : ι × α) ↦ (f' q.2, F' q.1 q.2))
    (SProd.sprod (β := Filter α) p ⊤) (𝓤 (↑s : Type u_2))

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
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.restrict (π := fun (a : β) ↦ γ) g)
F' : (i : ι) → α → (↑s : Type u_2)
hF' : (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) = F
f' : (i : α) → (↑s : Type u_2)
hf' : (fun (i : α) ↦ (↑(f' i) : β)) = f
comp_tendstoUniformly :
  ∀ (hF : ∀ (i : ι) (x : α), (↑(F' i x) : β) ∈ s) (hf : ∀ (x : α), (↑(f' x) : β) ∈ s) (hg : UniformContinuousOn g s)
    (h :
      TendstoUniformly.{u_1, u_2, u_4} (β := β) (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β))
        (fun (i : α) ↦ (↑(f' i) : β)) p),
    TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (↑(f' x) : β))
      p
h : Tendsto (fun (q : ι × α) ↦ ((↑(f' q.2) : β), (↑(F' q.1 q.2) : β))) (SProd.sprod (β := Filter α) p ⊤) (𝓤 β)
this :
  Tendsto (β := (↑s : Type u_2) × (↑s : Type u_2)) (fun (q : ι × α) ↦ (f' q.2, F' q.1 q.2))
    (SProd.sprod (β := Filter α) p ⊤) (𝓤 (↑s : Type u_2))
apply : TendstoUniformly F' f' p
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (↑(f' x) : β)) p

Tactic:
apply UniformContinuous.comp_tendstoUniformly hg ?_

Premises used: UniformContinuous.comp_tendstoUniformly
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hg : UniformContinuous (s.restrict (π := fun (a : β) ↦ γ) g)
F' : (i : ι) → α → (↑s : Type u_2)
hF' : (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) = F
f' : (i : α) → (↑s : Type u_2)
hf' : (fun (i : α) ↦ (↑(f' i) : β)) = f
comp_tendstoUniformly :
  ∀ (hF : ∀ (i : ι) (x : α), (↑(F' i x) : β) ∈ s) (hf : ∀ (x : α), (↑(f' x) : β) ∈ s) (hg : UniformContinuousOn g s)
    (h :
      TendstoUniformly.{u_1, u_2, u_4} (β := β) (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β))
        (fun (i : α) ↦ (↑(f' i) : β)) p),
    TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (↑(f' x) : β))
      p
h : Tendsto (fun (q : ι × α) ↦ ((↑(f' q.2) : β), (↑(F' q.1 q.2) : β))) (SProd.sprod (β := Filter α) p ⊤) (𝓤 β)
this :
  Tendsto (β := (↑s : Type u_2) × (↑s : Type u_2)) (fun (q : ι × α) ↦ (f' q.2, F' q.1 q.2))
    (SProd.sprod (β := Filter α) p ⊤) (𝓤 (↑s : Type u_2))
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : TendstoUniformly F' f' p), TendstoUniformly F' f' p
⊢ TendstoUniformly F' f' p

Tactic:
rwa [← tendstoUniformly_iff_tendsto] at this

Premises used: tendstoUniformly_iff_tendsto
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
obtain :
  ∀ (s' : Set ι) (hs' : s' ∈ p) (hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s),
    TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p

Tactic:
obtain ⟨s', hs', hs⟩ := eventually_iff_exists_mem.mp hF

Premises used: Iff.mp, Filter.eventually_iff_exists_mem
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
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
rw : ∃ s ∈ p, EqOn F F' s
⊢ F =ᶠ[p] F'

Tactic:
rw [eventuallyEq_iff_exists_mem]

Premises used: Filter.eventuallyEq_iff_exists_mem
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
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:
grind
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
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 grind⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
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:
have hF : F =ᶠ[p] F' := by
    rw [eventuallyEq_iff_exists_mem]
    refine ⟨s', hs', fun y hy => by grind⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF_1 : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
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'
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : TendstoUniformly F' f p) (hF : F =ᶠ[p] F'), TendstoUniformly F' f p
⊢ TendstoUniformly F' f p

Tactic:
rwa [tendstoUniformly_congr hF] at h

Premises used: tendstoUniformly_congr
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF_1 : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
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:
have h' : TendstoUniformly F' f p := by
    rwa [tendstoUniformly_congr hF] at h
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF_1 : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
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:
grind
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF_1 : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
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
apply : p.EventuallyEq (β := α → γ) (fun (i : ι) (x : α) ↦ g (F i x)) fun (i : ι) (x : α) ↦ g (F' i x)
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p

Tactic:
apply (tendstoUniformly_congr _).mpr
    (UniformContinuousOn.comp_tendstoUniformly (by grind) hf hg h')

Premises used: Iff.mpr, UniformContinuousOn.comp_tendstoUniformly, tendstoUniformly_congr
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF_1 : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
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
rw : ∃ s ∈ p, EqOn (β := α → γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (i : ι) (x : α) ↦ g (F' i x)) s
⊢ p.EventuallyEq (β := α → γ) (fun (i : ι) (x : α) ↦ g (F i x)) fun (i : ι) (x : α) ↦ g (F' i x)

Tactic:
rw [eventuallyEq_iff_exists_mem]

Premises used: Filter.eventuallyEq_iff_exists_mem
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF_1 : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
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'
⊢ Eq (α := α → γ) ((fun (i : ι) (x : α) ↦ g (F i x)) i) ((fun (i : ι) (x : α) ↦ g (F' i x)) i)

Tactic:
grind
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF_1 : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
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 grind⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
obtain :
  ∀ (s' : Set ι) (hs' : s' ∈ p) (hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s),
    TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p
obtain₁ :
  ∀ (s' : Set ι) (hs' : s' ∈ p) (hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s),
    TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p
obtain₂ :
  ∀ (s' : Set ι) (hs' : s' ∈ p) (hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s),
    let F' : ι → α → β := fun (i : ι) (x : α) ↦ if i ∈ s' then F i x else f x;
    ∀ (hF : F =ᶠ[p] F'),
      TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p
obtain₃ :
  ∀ (s' : Set ι) (hs' : s' ∈ p) (hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s),
    let F' : ι → α → β := fun (i : ι) (x : α) ↦ if i ∈ s' then F i x else f x;
    ∀ (hF : F =ᶠ[p] F') (h' : TendstoUniformly F' f p),
      TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p
obtain₄ :
  ∀ (s' : Set ι) (hs' : s' ∈ p) (hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s),
    let F' : ι → α → β := fun (i : ι) (x : α) ↦ if i ∈ s' then F i x else f x;
    ∀ (hF : F =ᶠ[p] F') (h' : TendstoUniformly F' f p),
      p.EventuallyEq (β := α → γ) (fun (i : ι) (x : α) ↦ g (F i x)) fun (i : ι) (x : α) ↦ g (F' i x)
obtain₅ :
  ∀ (s' : Set ι) (hs' : s' ∈ p) (hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s),
    let 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
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p

Tactic:
classical
  obtain ⟨s', hs', hs⟩ := eventually_iff_exists_mem.mp 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 grind⟩
  have h' : TendstoUniformly F' f p := by
    rwa [tendstoUniformly_congr hF] at h
  apply (tendstoUniformly_congr _).mpr
    (UniformContinuousOn.comp_tendstoUniformly (by grind) hf hg h')
  rw [eventuallyEq_iff_exists_mem]
  refine ⟨s', hs', fun i hi => by grind⟩

Premises used: Iff.mp, Filter.eventuallyEq_iff_exists_mem, Filter.eventually_iff_exists_mem
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
t : Set α
hF : ∀ᶠ (i : ι) in p, ∀ x ∈ t, F i x ∈ s
hf : ∀ x ∈ t, f x ∈ s
g : β → γ
hg : UniformContinuousOn g s
h : TendstoUniformlyOn F f p t
rw :
  TendstoUniformly.{u_1, u_3, u_4} (α := (↑t : Type u_1)) (β := γ)
    (fun (n : ι) ↦ t.restrict (π := fun (a : α) ↦ γ) fun (x : α) ↦ g (F n x))
    (t.restrict (π := fun (a : α) ↦ γ) fun (x : α) ↦ g (f x)) p
⊢ TendstoUniformlyOn.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p t

Tactic:
rw [tendstoUniformlyOn_iff_restrict]

Premises used: tendstoUniformlyOn_iff_restrict
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
t : Set α
hF : ∀ᶠ (i : ι) in p, ∀ x ∈ t, F i x ∈ s
hf : ∀ x ∈ t, f x ∈ s
g : β → γ
hg : UniformContinuousOn g s
h : TendstoUniformlyOn F f p t
⊢ ∀ᶠ (i : ι) in p, ∀ (x : (↑t : Type u_1)), t.restrict (π := fun (a : α) ↦ β) (F i) x ∈ s

Tactic:
simpa using hF
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
t : Set α
hF : ∀ᶠ (i : ι) in p, ∀ x ∈ t, F i x ∈ s
hf : ∀ x ∈ t, f x ∈ s
g : β → γ
hg : UniformContinuousOn g s
h : TendstoUniformlyOn F f p t
⊢ ∀ (x : (↑t : Type u_1)), t.restrict (π := fun (a : α) ↦ β) f x ∈ s

Tactic:
simpa using hf
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
t : Set α
hF : ∀ᶠ (i : ι) in p, ∀ x ∈ t, F i x ∈ s
hf : ∀ x ∈ t, f x ∈ s
g : β → γ
hg : UniformContinuousOn g s
h : TendstoUniformlyOn F f p t
⊢ TendstoUniformly.{u_1, u_3, u_4} (α := (↑t : Type u_1)) (β := γ)
    (fun (n : ι) ↦ t.restrict (π := fun (a : α) ↦ γ) fun (x : α) ↦ g (F n x))
    (t.restrict (π := fun (a : α) ↦ γ) fun (x : α) ↦ g (f x)) p

Tactic:
apply UniformContinuousOn.comp_tendstoUniformly_eventually (by simpa using hF)
     (by simpa using hf) hg (tendstoUniformlyOn_iff_restrict.mp h)

Premises used: UniformContinuousOn.comp_tendstoUniformly_eventually, tendstoUniformlyOn_iff_restrict, Iff.mp