awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (hypothesis)
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 ⊤) (𝓤 β)
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (↑(f' x) : β)) p
have 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))
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
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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))
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (↑(f' x) : β)) p
have apply : TendstoUniformly F' f' p
Tactic: apply UniformContinuous.comp_tendstoUniformly hg ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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))
⊢ TendstoUniformly F' f' p
have rwa : ∀ (this : TendstoUniformly F' f' p), TendstoUniformly F' f' p
Tactic: rwa [← tendstoUniformly_iff_tendsto] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p
have 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
Tactic: obtain ⟨s', hs', hs⟩ := eventually_iff_exists_mem.mp hF
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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'
have rw : ∃ s ∈ p, EqOn F F' s
Tactic: rw [eventuallyEq_iff_exists_mem]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (hypothesis)
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
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p
have hF₁ : F =ᶠ[p] F'
Tactic: have hF : F =ᶠ[p] F' := by
    rw [eventuallyEq_iff_exists_mem]
    refine ⟨s', hs', fun y hy => by grind⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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
have rwa : ∀ (h : TendstoUniformly F' f p) (hF : F =ᶠ[p] F'), TendstoUniformly F' f p
Tactic: rwa [tendstoUniformly_congr hF] at h
Cleared hypotheses: h, hF
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (hypothesis)
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.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p
have h' : TendstoUniformly F' f p
Tactic: have h' : TendstoUniformly F' f p := by
    rwa [tendstoUniformly_congr hF] at h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p
have apply : p.EventuallyEq (β := α → γ) (fun (i : ι) (x : α) ↦ g (F i x)) fun (i : ι) (x : α) ↦ g (F' i x)
Tactic: apply (tendstoUniformly_congr _).mpr
    (UniformContinuousOn.comp_tendstoUniformly (by grind) hf hg h')
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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
⊢ p.EventuallyEq (β := α → γ) (fun (i : ι) (x : α) ↦ g (F i x)) fun (i : ι) (x : α) ↦ g (F' i x)
have rw : ∃ s ∈ p, EqOn (β := α → γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (i : ι) (x : α) ↦ g (F' i x)) s
Tactic: rw [eventuallyEq_iff_exists_mem]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p
have 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
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⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p
have 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
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⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p
have 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
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⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p
have 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)
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⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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)
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p
have 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
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⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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
⊢ TendstoUniformlyOn.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p t
have 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
Tactic: rw [tendstoUniformlyOn_iff_restrict]