awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
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
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:
hvu <| prodMk_mem_comp (prodMk_mem_comp (hFv _ x.1.prop) hx)
      <| hvsymm.symm (f x.2) (F x.2) <| hFv _ x.2.prop

Premises used: Std.Symm.symm, Prod.fst, Subtype.prop, SetRel.prodMk_mem_comp, Subtype.val, Prod.snd
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
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
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:
exact hvu <| prodMk_mem_comp (prodMk_mem_comp (hFv _ x.1.prop) hx)
      <| hvsymm.symm (f x.2) (F x.2) <| hFv _ x.2.prop

Premises used: Std.Symm.symm, Prod.fst, Subtype.prop, SetRel.prodMk_mem_comp, Subtype.val, Prod.snd
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_4
β : Type u_5
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
h : ∀ u ∈ 𝓤 β, ∃ (F : α → β), UniformContinuous F ∧ ∀ (y : α), (f y, F y) ∈ u
⊢ ∀ u ∈ 𝓤 β, ∃ (F : α → β), UniformContinuousOn F univ ∧ ∀ (y : α), Membership.mem (γ := Set α) univ y → (f y, F y) ∈ u

Tactic:
simpa [uniformContinuousOn_univ] using h

Premises used: uniformContinuousOn_univ
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_4
β : Type u_5
ι : Type u_6
inst : UniformSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoUniformlyOn F f p s
hc : ∃ᶠ (n : ι) in p, UniformContinuousOn (F n) s
⊢ UniformContinuousOn f s

Tactic:
uniformContinuousOn_of_uniform_approx_of_uniformContinuousOn fun u hu ↦
    let ⟨i, hF⟩ := (hc.and_eventually (h u hu)).exists
    ⟨F i, hF⟩

Premises used: uniformContinuousOn_of_uniform_approx_of_uniformContinuousOn, _private.0.TendstoUniformlyOn.uniformContinuousOn.match_1, Exists, Filter.Frequently.and_eventually, And, Filter.Frequently.exists, Exists.intro, UniformContinuousOn
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_4
β : Type u_5
ι : Type u_6
inst : UniformSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : TendstoUniformly F f p
hc : ∃ᶠ (n : ι) in p, UniformContinuous (F n)
⊢ UniformContinuous f

Tactic:
uniformContinuous_of_uniform_approx_of_uniformContinuous fun u hu ↦
    let ⟨i, hF⟩ := (hc.and_eventually (h u hu)).exists
    ⟨F i, hF⟩

Premises used: UniformContinuous, Exists, uniformContinuous_of_uniform_approx_of_uniformContinuous, Filter.Frequently.and_eventually, And, Filter.Frequently.exists, Exists.intro, _private.0.TendstoUniformly.uniformContinuous.match_1
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
⊢ TendstoUniformlyOnFilter F f p p' ↔ Tendsto (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, TendstoUniformlyOnFilter, Set.preimage, Filter.Tendsto
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
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
⊢ (∀ 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

Tactic:
apply forall₂_congr

Premises used: forall₂_congr
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : ∀ (a : Set (β × β)) (b : a ∈ 𝓤 β), True
⊢ ∀ (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:
simp_rw [eventually_prod_principal_iff]

Premises used: Filter.eventually_prod_principal_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ ∀ (a : Set (β × β)) (b : a ∈ 𝓤 β), True

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ TendstoUniformlyOn F f p s ↔ Tendsto (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)

Tactic:
simp [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, tendstoUniformlyOnFilter_iff_tendsto]

Premises used: tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, tendstoUniformlyOnFilter_iff_tendsto
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoUniformlyOn F f p univ ↔ TendstoUniformly F f p

Tactic:
simp [TendstoUniformlyOn, TendstoUniformly]

Premises used: TendstoUniformlyOn, TendstoUniformly
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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 ⊤
rw₂ rw₃ : TendstoUniformlyOnFilter F f p ⊤ ↔ TendstoUniformlyOnFilter F f p ⊤
⊢ TendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤

Tactic:
rw [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, principal_univ]

Premises used: tendstoUniformlyOn_univ, tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, Filter.principal_univ
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h rwa rwa₁ rwa₂ rwa₃ : TendstoUniformly F f p
⊢ TendstoUniformlyOnFilter F f p ⊤

Tactic:
rwa [← tendstoUniformly_iff_tendstoUniformlyOnFilter]

Premises used: tendstoUniformly_iff_tendstoUniformlyOnFilter
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
u : Set (β × β)
h : u ∈ 𝓤 β
⊢ (∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u) ↔
    ∀ᶠ (n : ι) in p,
      ∀ (x : (↑s : Type u_1)),
        ((f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) x, (fun (i : ι) (x : (↑s : Type u_1)) ↦ F i (↑x : α)) n x) ∈ u

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
K : Set α
⊢ TendstoUniformlyOn F f p K ↔
    TendstoUniformly (fun (n : ι) ↦ K.restrict (π := fun (a : α) ↦ β) (F n)) (K.restrict (π := fun (a : α) ↦ β) f) p

Tactic:
tendstoUniformlyOn_iff_tendstoUniformly_comp_coe

Premises used: tendstoUniformlyOn_iff_tendstoUniformly_comp_coe, Set.restrict
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoUniformly F f p ↔ Tendsto (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) (SProd.sprod (β := Filter α) p ⊤) (𝓤 β)

Tactic:
simp [tendstoUniformly_iff_tendstoUniformlyOnFilter, tendstoUniformlyOnFilter_iff_tendsto]

Premises used: tendstoUniformly_iff_tendstoUniformlyOnFilter, tendstoUniformlyOnFilter_iff_tendsto
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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))

Tactic:
Uniform.tendsto_nhds_right.mpr fun u hu => mem_map.mpr ?_

Premises used: Iff.mpr, Uniform.tendsto_nhds_right, Filter.mem_map
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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'
refine : ∀ (u : Set (β × β)) (hu : u ∈ 𝓤 β), (fun (x_1 : ι) ↦ (f x, F x_1 x)) ⁻¹' u ∈ p
⊢ Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))

Tactic:
refine Uniform.tendsto_nhds_right.mpr fun u hu => mem_map.mpr ?_

Premises used: Iff.mpr, Uniform.tendsto_nhds_right, Filter.mem_map
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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 ∈ 𝓤 β
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
⊢ (fun (x_1 : ι) ↦ (f x, F x_1 x)) ⁻¹' u ∈ p

Tactic:
filter_upwards [(h u hu).curry]

Premises used: Filter.Eventually.curry
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
p' : Filter α
h_1 : TendstoUniformlyOnFilter F f p p'
hx : 𝓟 {x} ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
i : ι
h : ∀ᶠ (y : α) in p', (f y, F i y) ∈ u
⊢ Membership.mem (γ := Set ι) ((fun (x_1 : ι) ↦ (f x, F x_1 x)) ⁻¹' u) i

Tactic:
simpa using h.filter_mono hx

Premises used: Filter.Eventually.filter_mono
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
x : α
p : Filter ι
h : TendstoUniformlyOn F f p s
hx : x ∈ s
⊢ Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))

Tactic:
h.tendstoUniformlyOnFilter.tendsto_at
    (le_principal_iff.mpr <| mem_principal.mpr <| singleton_subset_iff.mpr <| hx)

Premises used: Iff.mpr, Set.singleton_subset_iff, Filter.le_principal_iff, TendstoUniformlyOnFilter.tendsto_at, Filter.mem_principal, TendstoUniformlyOn.tendstoUniformlyOnFilter
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : TendstoUniformly F f p
x : α
⊢ Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))

Tactic:
h.tendstoUniformlyOnFilter.tendsto_at le_top

Premises used: TendstoUniformlyOnFilter.tendsto_at, TendstoUniformly.tendstoUniformlyOnFilter, le_top
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
p'' : Filter ι
h : TendstoUniformlyOnFilter F f p p'
hp : p'' ≤ p
⊢ TendstoUniformlyOnFilter F f p'' p'

Tactic:
fun u hu =>
  (h u hu).filter_mono (p'.prod_mono_left hp)

Premises used: Filter.Eventually.filter_mono, TendstoUniformlyOnFilter, Filter.prod_mono_left
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' p'' : Filter α
h : TendstoUniformlyOnFilter F f p p'
hp : p'' ≤ p'
⊢ TendstoUniformlyOnFilter F f p p''

Tactic:
fun u hu =>
  (h u hu).filter_mono (p.prod_mono_right hp)

Premises used: Filter.Eventually.filter_mono, TendstoUniformlyOnFilter, Filter.prod_mono_right
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
h : TendstoUniformlyOn F f p s
h' : s' ⊆ s
⊢ TendstoUniformlyOn F f p s'

Tactic:
tendstoUniformlyOn_iff_tendstoUniformlyOnFilter.mpr
    (h.tendstoUniformlyOnFilter.mono_right (le_principal_iff.mpr <| mem_principal.mpr h'))

Premises used: Iff.mpr, TendstoUniformlyOnFilter.mono_right, Filter.le_principal_iff, tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, Filter.mem_principal, TendstoUniformlyOn.tendstoUniformlyOnFilter
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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)
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
⊢ TendstoUniformlyOnFilter F' f p p'

Tactic:
rw [tendstoUniformlyOnFilter_iff_tendsto, uniformity_hasBasis_open.tendsto_right_iff] at hf ⊢

Premises used: tendstoUniformlyOnFilter_iff_tendsto, Filter.HasBasis.tendsto_right_iff, uniformity_hasBasis_open
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
F' : ι → α → β
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:
fun i hi => (hf i hi).congr (hff'.mono fun x hx =>
    (Inseparable.rfl.prod hx).mem_open_iff hi.2)

Premises used: Inseparable.rfl, Filter.Eventually.mono, And.right, Filter.Eventually.congr, Inseparable.prod, Inseparable.mem_open_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
F' : ι → α → β
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:
exact fun i hi => (hf i hi).congr (hff'.mono fun x hx =>
    (Inseparable.rfl.prod hx).mem_open_iff hi.2)

Premises used: Inseparable.rfl, Filter.Eventually.mono, And.right, Filter.Eventually.congr, Inseparable.prod, Inseparable.mem_open_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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', F n.1 n.2 = F' n.1 n.2
⊢ TendstoUniformlyOnFilter F' f p p'

Tactic:
hf.congr_inseparable (hff'.mono fun _ h => .of_eq h)

Premises used: Inseparable.of_eq, Filter.Eventually.mono, TendstoUniformlyOnFilter.congr_inseparable
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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)
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)
⊢ TendstoUniformlyOn F' f p s

Tactic:
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter] at hf ⊢

Premises used: tendstoUniformlyOn_iff_tendstoUniformlyOnFilter
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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)

Tactic:
hf.congr_inseparable ?_

Premises used: TendstoUniformlyOnFilter.congr_inseparable
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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)
refine : ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, Inseparable (F n.1 n.2) (F' n.1 n.2)
⊢ TendstoUniformlyOnFilter F' f p (𝓟 s)

Tactic:
refine hf.congr_inseparable ?_

Premises used: TendstoUniformlyOnFilter.congr_inseparable
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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)
rwa rwa₁ rwa₂ rwa₃ : ∀ᶠ (x : ι) in p, ∀ y ∈ s, Inseparable (F (x, y).1 (x, y).2) (F' (x, y).1 (x, y).2)
⊢ ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, Inseparable (F n.1 n.2) (F' n.1 n.2)

Tactic:
rwa [eventually_prod_principal_iff]

Premises used: Filter.eventually_prod_principal_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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, EqOn (F n) (F' n) s
⊢ TendstoUniformlyOn F' f p s

Tactic:
hf.congr_inseparable (hff'.mono fun _ h _ hx => .of_eq (h hx))

Premises used: TendstoUniformlyOn.congr_inseparable, Inseparable.of_eq, Filter.Eventually.mono
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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)
rw : TendstoUniformlyOn F f p univ ↔ TendstoUniformlyOn F' f p univ
⊢ TendstoUniformly F f p ↔ TendstoUniformly F' f p

Tactic:
rw [← tendstoUniformlyOn_univ, ← tendstoUniformlyOn_univ]

Premises used: tendstoUniformlyOn_univ
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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)
⊢ TendstoUniformlyOn F f p univ ↔ TendstoUniformlyOn F' f p univ

Tactic:
⟨fun h => h.congr_inseparable (hF.mono fun _ hx y _ => hx y),
    fun h => h.congr_inseparable (hF.mono fun _ hx y _ => (hx y).symm)⟩

Premises used: TendstoUniformlyOn.congr_inseparable, Filter.Eventually.mono, Inseparable.symm, Iff.intro
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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)
⊢ TendstoUniformlyOn F f p univ ↔ TendstoUniformlyOn F' f p univ

Tactic:
exact ⟨fun h => h.congr_inseparable (hF.mono fun _ hx y _ => hx y),
    fun h => h.congr_inseparable (hF.mono fun _ hx y _ => (hx y).symm)⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
F' : ι → α → β
hF : F =ᶠ[p] F'
⊢ TendstoUniformly F f p ↔ TendstoUniformly F' f p

Tactic:
tendstoUniformly_congr_inseparable (hF.mono fun _ hx y => .of_eq (congrFun hx y))

Premises used: tendstoUniformly_congr_inseparable, Inseparable.of_eq, Filter.Eventually.mono, congrFun
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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)
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
⊢ TendstoUniformlyOn F g p s

Tactic:
rw [tendstoUniformlyOn_iff_tendsto, uniformity_hasBasis_open.tendsto_right_iff] at hf ⊢

Premises used: tendstoUniformlyOn_iff_tendsto, Filter.HasBasis.tendsto_right_iff, uniformity_hasBasis_open
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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

Tactic:
forall₂_imp (fun i hi hf => ?_) hf

Premises used: forall₂_imp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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)
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
⊢ ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (g x.2, F x.1 x.2) ∈ id i

Tactic:
refine forall₂_imp (fun i hi hf => ?_) hf

Premises used: forall₂_imp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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
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
⊢ ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (g x.2, F x.1 x.2) ∈ id i

Tactic:
rw [eventually_prod_principal_iff] at hf ⊢

Premises used: Filter.eventually_prod_principal_iff