awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
x : α
hx : x ∈ s
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
u₂ : Set (β × β)
h₂ : u₂ ∈ 𝓤 β
hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂
u₂₁ : u₂ ○ u₂ ⊆ u₁
t : Set α
tx : t ∈ 𝓝[s] x
F : α → β
hFc : ContinuousWithinAt F s x
hF : ∀ y ∈ t, (f y, F y) ∈ u₂
A : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F y) ∈ u₂
B : ∀ᶠ (y : α) in 𝓝[s] x, (F y, F x) ∈ u₂
C : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F x) ∈ u₁
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : α) ↦ (f x_1, f x)) (𝓝[s] x)) u₀
have this : (F x, f x) ∈ u₁
Tactic: have : (F x, f x) ∈ u₁ :=
    u₂₁ (prodMk_mem_comp (refl_mem_uniformity h₂) (hsymm (A.self_of_nhdsWithin hx)))
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : α → β
x : α
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ (F : α → β), ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ ContinuousAt f x
have rw : ContinuousWithinAt f univ x
Tactic: rw [← continuousWithinAt_univ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : α → β
x : α
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ (F : α → β), ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ ContinuousWithinAt f univ x
have apply : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[univ] x, ∃ (F : α → β), ContinuousWithinAt F univ x ∧ ∀ y ∈ t, (f y, F y) ∈ u
Tactic: apply continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt (mem_univ _) _
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
hc : ∃ᶠ (n : ι) in p, ContinuousOn (F n) s
⊢ ContinuousOn f s
have refine : ∀ (x : α) (hx : x ∈ s) (u : Set (β × β)) (hu : u ∈ 𝓤 β),
  ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
Tactic: refine continuousOn_of_locally_uniform_approx_of_continuousWithinAt fun x hx u hu => ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
hc : ∃ᶠ (n : ι) in p, ContinuousOn (F n) s
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
have rcases : ∀ (t : Set α) (ht : t ∈ 𝓝[s] x) (H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u),
  ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
Tactic: rcases h u hu x hx with ⟨t, ht, H⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
hc : ∃ᶠ (n : ι) in p, ContinuousOn (F n) s
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
have rcases : ∀ (n : ι) (hFc : ContinuousOn (F n) s) (hF : ∀ y ∈ t, (f y, F n y) ∈ u),
  ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
Tactic: rcases (hc.and_eventually H).exists with ⟨n, hFc, hF⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f s x
hg : Tendsto g p (𝓝[s] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun (n : ι) ↦ F n (g n)) p (𝓝 (f x))
have refine : ∀ (u₀ : Set (β × β)) (hu₀ : u₀ ∈ 𝓤 β),
  Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : ι) ↦ (f x, F x_1 (g x_1))) p) u₀
Tactic: refine Uniform.tendsto_nhds_right.2 fun u₀ hu₀ => ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f s x
hg : Tendsto g p (𝓝[s] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : ι) ↦ (f x, F x_1 (g x_1))) p) u₀
have obtain : ∀ (u₁ : Set (β × β)) (h₁ : u₁ ∈ 𝓤 β) (u₁₀ : u₁ ○ u₁ ⊆ u₀),
  Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : ι) ↦ (f x, F x_1 (g x_1))) p) u₀
Tactic: obtain ⟨u₁, h₁, u₁₀⟩ : ∃ u ∈ 𝓤 β, u ○ u ⊆ u₀ := comp_mem_uniformity_sets hu₀
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f s x
hg : Tendsto g p (𝓝[s] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : ι) ↦ (f x, F x_1 (g x_1))) p) u₀
have rcases : ∀ (s_1 : Set α) (sx : s_1 ∈ 𝓝[s] x) (hs : ∀ᶠ (n : ι) in p, ∀ y ∈ s_1, (f y, F n y) ∈ u₁),
  Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : ι) ↦ (f x, F x_1 (g x_1))) p) u₀
Tactic: rcases hunif u₁ h₁ with ⟨s, sx, hs⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s_1 : Set α
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f s_1 x
hg : Tendsto g p (𝓝[s_1] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s_1] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
s : Set α
sx : s ∈ 𝓝[s_1] x
hs : ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, F n y) ∈ u₁
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : ι) ↦ (f x, F x_1 (g x_1))) p) u₀
have A : ∀ᶠ (n : ι) in p, g n ∈ s
Tactic: have A : ∀ᶠ n in p, g n ∈ s := hg sx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s_1 : Set α
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f s_1 x
hg : Tendsto g p (𝓝[s_1] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s_1] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
s : Set α
sx : s ∈ 𝓝[s_1] x
hs : ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, F n y) ∈ u₁
A : ∀ᶠ (n : ι) in p, g n ∈ s
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : ι) ↦ (f x, F x_1 (g x_1))) p) u₀
have B : ∀ᶠ (n : ι) in p, (f x, f (g n)) ∈ u₁
Tactic: have B : ∀ᶠ n in p, (f x, f (g n)) ∈ u₁ := hg (Uniform.continuousWithinAt_iff'_right.1 h h₁)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
h : ContinuousAt f x
hg : Tendsto g p (𝓝 x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun (n : ι) ↦ F n (g n)) p (𝓝 (f x))
have h₁ : ContinuousWithinAt f univ x
Tactic: rw [← continuousWithinAt_univ] at h
Cleared hypotheses: h, hg, hunif
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝 x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun (n : ι) ↦ F n (g n)) p (𝓝 (f x))
have hg₁ : Tendsto g p (𝓝[univ] x)
Tactic: rw [← nhdsWithin_univ] at hunif hg
Cleared hypotheses: hg, hunif
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝 x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
hg₁ : Tendsto g p (𝓝[univ] x)
⊢ Tendsto (fun (n : ι) ↦ F n (g n)) p (𝓝 (f x))
have hunif₁ : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[univ] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
Tactic: rw [← nhdsWithin_univ] at hunif hg
Cleared hypotheses: hg, hunif
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (goal)
Goal:
α : Type u_4
β : Type u_5
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
h : ∀ u ∈ 𝓤 β, ∃ (F : α → β), UniformContinuousOn F s ∧ ∀ y ∈ s, (f y, F y) ∈ u
⊢ UniformContinuousOn f s
have simp_rw : ∀
  (h :
    ∀ u ∈ 𝓤 β,
      ∃ (F : α → β),
        (∀ r ∈ 𝓤 β,
            Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
              {x : (↑s : Type u_4) × (↑s : Type u_4) |
                (s.restrict (π := fun (a : α) ↦ β) F x.1, s.restrict (π := fun (a : α) ↦ β) F x.2) ∈ r}) ∧
          ∀ y ∈ s, (f y, F y) ∈ u),
  ∀ r ∈ 𝓤 β,
    Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
      {x : (↑s : Type u_4) × (↑s : Type u_4) |
        (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2) ∈ r}
Tactic: simp_rw [uniformContinuousOn_iff_restrict, uniformContinuous_def] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (goal)
Goal:
α : Type u_4
β : Type u_5
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
h :
  ∀ u ∈ 𝓤 β,
    ∃ (F : α → β),
      (∀ r ∈ 𝓤 β,
          Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
            {x : (↑s : Type u_4) × (↑s : Type u_4) |
              (s.restrict (π := fun (a : α) ↦ β) F x.1, s.restrict (π := fun (a : α) ↦ β) F x.2) ∈ r}) ∧
        ∀ y ∈ s, (f y, F y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
    {x : (↑s : Type u_4) × (↑s : Type u_4) |
      (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2) ∈ u}
have obtain : ∀ (v : Set (β × β)) (hv : v ∈ 𝓤 β) (hvsymm : SetRel.IsSymm v) (hvu : v ○ v ○ v ⊆ u),
  Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
    {x : (↑s : Type u_4) × (↑s : Type u_4) |
      (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2) ∈ u}
Tactic: obtain ⟨v, hv, hvsymm, hvu⟩ := comp_comp_symm_mem_uniformity_sets hu
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (goal)
Goal:
α : Type u_4
β : Type u_5
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
h :
  ∀ u ∈ 𝓤 β,
    ∃ (F : α → β),
      (∀ r ∈ 𝓤 β,
          Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
            {x : (↑s : Type u_4) × (↑s : Type u_4) |
              (s.restrict (π := fun (a : α) ↦ β) F x.1, s.restrict (π := fun (a : α) ↦ β) F x.2) ∈ r}) ∧
        ∀ y ∈ s, (f y, F y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
v : Set (β × β)
hv : v ∈ 𝓤 β
hvsymm : SetRel.IsSymm v
hvu : v ○ v ○ v ⊆ u
⊢ Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
    {x : (↑s : Type u_4) × (↑s : Type u_4) |
      (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2) ∈ u}
have obtain : ∀ (F : α → β)
  (hF :
    ∀ r ∈ 𝓤 β,
      Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
        {x : (↑s : Type u_4) × (↑s : Type u_4) |
          (s.restrict (π := fun (a : α) ↦ β) F x.1, s.restrict (π := fun (a : α) ↦ β) F x.2) ∈ r})
  (hFv : ∀ y ∈ s, (f y, F y) ∈ v),
  Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
    {x : (↑s : Type u_4) × (↑s : Type u_4) |
      (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2) ∈ u}
Tactic: obtain ⟨F, hF, hFv⟩ := h v hv
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (goal)
Goal:
α : Type u_4
β : Type u_5
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
h :
  ∀ u ∈ 𝓤 β,
    ∃ (F : α → β),
      (∀ r ∈ 𝓤 β,
          Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
            {x : (↑s : Type u_4) × (↑s : Type u_4) |
              (s.restrict (π := fun (a : α) ↦ β) F x.1, s.restrict (π := fun (a : α) ↦ β) F x.2) ∈ r}) ∧
        ∀ y ∈ s, (f y, F y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
v : Set (β × β)
hv : v ∈ 𝓤 β
hvsymm : SetRel.IsSymm v
hvu : v ○ v ○ v ⊆ u
F : α → β
hF :
  ∀ r ∈ 𝓤 β,
    Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
      {x : (↑s : Type u_4) × (↑s : Type u_4) |
        (s.restrict (π := fun (a : α) ↦ β) F x.1, s.restrict (π := fun (a : α) ↦ β) F x.2) ∈ r}
hFv : ∀ y ∈ s, (f y, F y) ∈ v
⊢ Membership.mem (γ := Filter ((↑s : Type u_4) × (↑s : Type u_4))) (𝓤 (↑s : Type u_4))
    {x : (↑s : Type u_4) × (↑s : Type u_4) |
      (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2) ∈ u}
have h₁ : ∀ (x : (↑s : Type u_4) × (↑s : Type u_4))
  (hx : (s.restrict (π := fun (a : α) ↦ β) F x.1, s.restrict (π := fun (a : α) ↦ β) F x.2) ∈ v),
  (s.restrict (π := fun (a : α) ↦ β) f x.1, s.restrict (π := fun (a : α) ↦ β) f x.2) ∈ u
Tactic: filter_upwards [hF v hv] with x hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ (∀ u ∈ 𝓤 β, ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u) ↔
    ∀ u ∈ 𝓤 β, ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, (f n.2, F n.1 n.2) ∈ u
have h : ∀ (a : Set (β × β)) (b : a ∈ 𝓤 β),
  (∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ a) ↔ ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, (f n.2, F n.1 n.2) ∈ a
Tactic: apply forall₂_congr
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ ∀ (a : Set (β × β)) (b : a ∈ 𝓤 β),
    (∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ a) ↔ ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, (f n.2, F n.1 n.2) ∈ a
have h : ∀ (a : Set (β × β)) (b : a ∈ 𝓤 β), True
Tactic: simp_rw [eventually_prod_principal_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤
have rw : TendstoUniformlyOn F f p univ ↔ TendstoUniformlyOnFilter F f p ⊤
Tactic: rw [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, principal_univ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
rw : TendstoUniformlyOn F f p univ ↔ TendstoUniformlyOnFilter F f p ⊤
⊢ TendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤
have rw₁ : TendstoUniformlyOnFilter F f p (𝓟 univ) ↔ TendstoUniformlyOnFilter F f p ⊤
Tactic: rw [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, principal_univ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
rw : TendstoUniformlyOn F f p univ ↔ TendstoUniformlyOnFilter F f p ⊤
rw₁ : TendstoUniformlyOnFilter F f p (𝓟 univ) ↔ TendstoUniformlyOnFilter F f p ⊤
⊢ TendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤
have rw₂ : TendstoUniformlyOnFilter F f p ⊤ ↔ TendstoUniformlyOnFilter F f p ⊤
Tactic: rw [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, principal_univ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
p' : Filter α
h : TendstoUniformlyOnFilter F f p p'
hx : 𝓟 {x} ≤ p'
⊢ Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
have refine : ∀ (u : Set (β × β)) (hu : u ∈ 𝓤 β), (fun (x_1 : ι) ↦ (f x, F x_1 x)) ⁻¹' u ∈ p
Tactic: refine Uniform.tendsto_nhds_right.mpr fun u hu => mem_map.mpr ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
p' : Filter α
h : TendstoUniformlyOnFilter F f p p'
hx : 𝓟 {x} ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ (fun (x_1 : ι) ↦ (f x, F x_1 x)) ⁻¹' u ∈ p
have h₁ : ∀ (a : ι), (∀ᶠ (y : α) in p', (f y, F a y) ∈ u) → Membership.mem (γ := Set ι) ((fun (x_1 : ι) ↦ (f x, F x_1 x)) ⁻¹' u) a
Tactic: filter_upwards [(h u hu).curry]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p p'
hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', Inseparable (F n.1 n.2) (F' n.1 n.2)
⊢ TendstoUniformlyOnFilter F' f p p'
have rw : ∀
  (hf :
    ∀ (i : SetRel β β),
      i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ p', (f x.2, F x.1 x.2) ∈ id i)
  (hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', Inseparable (F n.1 n.2) (F' n.1 n.2)) (i : SetRel β β),
  i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ p', (f x.2, F' x.1 x.2) ∈ id i
Tactic: rw [tendstoUniformlyOnFilter_iff_tendsto, uniformity_hasBasis_open.tendsto_right_iff] at hf ⊢
Cleared hypotheses: hf, hff'
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
F' : ι → α → β
hf : TendstoUniformlyOn F f p s
hff' : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (F' n x)
⊢ TendstoUniformlyOn F' f p s
have rw : ∀ (hf : TendstoUniformlyOnFilter F f p (𝓟 s)) (hff' : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (F' n x)),
  TendstoUniformlyOnFilter F' f p (𝓟 s)
Tactic: rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter] at hf ⊢
Cleared hypotheses: hf, hff'
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p (𝓟 s)
hff' : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (F' n x)
⊢ TendstoUniformlyOnFilter F' f p (𝓟 s)
have refine : ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, Inseparable (F n.1 n.2) (F' n.1 n.2)
Tactic: refine hf.congr_inseparable ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p (𝓟 s)
hff' : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (F' n x)
⊢ ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, Inseparable (F n.1 n.2) (F' n.1 n.2)
have rwa : ∀ᶠ (x : ι) in p, ∀ y ∈ s, Inseparable (F (x, y).1 (x, y).2) (F' (x, y).1 (x, y).2)
Tactic: rwa [eventually_prod_principal_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
F' : ι → α → β
hF : ∀ᶠ (x : ι) in p, ∀ (y : α), Inseparable (F x y) (F' x y)
⊢ TendstoUniformly F f p ↔ TendstoUniformly F' f p
have rw : TendstoUniformlyOn F f p univ ↔ TendstoUniformlyOn F' f p univ
Tactic: rw [← tendstoUniformlyOn_univ, ← tendstoUniformlyOn_univ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : TendstoUniformlyOn F f p s
hfg : ∀ x ∈ s, Inseparable (f x) (g x)
⊢ TendstoUniformlyOn F g p s
have rw : ∀
  (hf :
    ∀ (i : SetRel β β),
      i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (f x.2, F x.1 x.2) ∈ id i)
  (hfg : ∀ x ∈ s, Inseparable (f x) (g x)) (i : SetRel β β),
  i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (g x.2, F x.1 x.2) ∈ id i
Tactic: rw [tendstoUniformlyOn_iff_tendsto, uniformity_hasBasis_open.tendsto_right_iff] at hf ⊢
Cleared hypotheses: hf, hfg
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf :
  ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (f x.2, F x.1 x.2) ∈ id i
hfg : ∀ x ∈ s, Inseparable (f x) (g x)
⊢ ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (g x.2, F x.1 x.2) ∈ id i
have refine : ∀ (i : SetRel β β) (hi : i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i)
  (hf : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (f x.2, F x.1 x.2) ∈ id i), ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (g x.2, F x.1 x.2) ∈ id i
Tactic: refine forall₂_imp (fun i hi hf => ?_) hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf_1 :
  ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (f x.2, F x.1 x.2) ∈ id i
hfg : ∀ x ∈ s, Inseparable (f x) (g x)
i : SetRel β β
hi : i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i
hf : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (f x.2, F x.1 x.2) ∈ id i
⊢ ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (g x.2, F x.1 x.2) ∈ id i
have rw : ∀ (hf : ∀ᶠ (x : ι) in p, ∀ y ∈ s, (f (x, y).2, F (x, y).1 (x, y).2) ∈ id i),
  ∀ᶠ (x : ι) in p, ∀ y ∈ s, (g (x, y).2, F (x, y).1 (x, y).2) ∈ id i
Tactic: rw [eventually_prod_principal_iff] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
h : TendstoUniformlyOnFilter F f p p'
g : γ → α
⊢ TendstoUniformlyOnFilter (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p (comap g p')
have rw : ∀ (h : Tendsto (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)) (g : γ → α),
  Tendsto (fun (q : ι × γ) ↦ ((f ∘ g) q.2, (F q.1 ∘ g) q.2)) (p ×ˢ comap g p') (𝓤 β)
Tactic: rw [tendstoUniformlyOnFilter_iff_tendsto] at h ⊢
Cleared hypotheses: h, g
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoUniformlyOn F f p s
g : γ → α
⊢ TendstoUniformlyOn (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p (g ⁻¹' s)
have rw : ∀ (h : TendstoUniformlyOnFilter F f p (𝓟 s)) (g : γ → α),
  TendstoUniformlyOnFilter (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p (𝓟 (g ⁻¹' s))
Tactic: rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter] at h ⊢
Cleared hypotheses: h, g
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : TendstoUniformly F f p
g : γ → α
⊢ TendstoUniformly (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p
have rw : ∀ (h : TendstoUniformlyOnFilter F f p ⊤) (g : γ → α), TendstoUniformlyOnFilter (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p ⊤
Tactic: rw [tendstoUniformly_iff_tendstoUniformlyOnFilter] at h ⊢
Cleared hypotheses: h, g