awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
simp :
  TendstoLocallyUniformlyOn F f p s ↔
    ∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ (pa : ι → Prop),
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
⊢ TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, TendstoUniformlyOnFilter F f p (𝓝[s] x)

Tactic:
simp only [TendstoUniformlyOnFilter, eventually_prod_iff]

Premises used: TendstoUniformlyOnFilter, Filter.eventually_prod_iff
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
mp :
  TendstoLocallyUniformlyOn F f p s →
    ∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ (pa : ι → Prop),
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
mpr :
  (∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ (pa : ι → Prop),
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u) →
    TendstoLocallyUniformlyOn F f p s
⊢ TendstoLocallyUniformlyOn F f p s ↔
    ∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ (pa : ι → Prop),
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
mp :
  ∀ (s_1 : Set α) (hs1 : s_1 ∈ 𝓝[s] x) (hs2 : ∀ᶠ (n : ι) in p, ∀ y ∈ s_1, (f y, F n y) ∈ u),
    ∃ (pa : ι → Prop),
      (∀ᶠ (x : ι) in p, pa x) ∧
        ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
⊢ ∃ (pa : ι → Prop),
    (∀ᶠ (x : ι) in p, pa x) ∧
      ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u

Tactic:
obtain ⟨s, hs1, hs2⟩ := h u hu x hx
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s_1 : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s_1
x : α
hx : x ∈ s_1
u : Set (β × β)
hu : u ∈ 𝓤 β
s : Set α
hs1 : s ∈ 𝓝[s_1] x
hs2 : ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, F n y) ∈ u
⊢ ∃ (pa : ι → Prop),
    (∀ᶠ (x : ι) in p, pa x) ∧
      ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s_1] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u

Tactic:
⟨_, hs2, _, eventually_of_mem hs1 fun x => id, fun hi y hy => hi y hy⟩

Premises used: id, Filter.eventually_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s_1 : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s_1
x : α
hx : x ∈ s_1
u : Set (β × β)
hu : u ∈ 𝓤 β
s : Set α
hs1 : s ∈ 𝓝[s_1] x
hs2 : ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, F n y) ∈ u
⊢ ∃ (pa : ι → Prop),
    (∀ᶠ (x : ι) in p, pa x) ∧
      ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s_1] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u

Tactic:
exact ⟨_, hs2, _, eventually_of_mem hs1 fun x => id, fun hi y hy => hi y hy⟩
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h :
  ∀ x ∈ s,
    ∀ u ∈ 𝓤 β,
      ∃ (pa : ι → Prop),
        (∀ᶠ (x : ι) in p, pa x) ∧
          ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
mpr :
  ∀ (pa : ι → Prop) (hpa : ∀ᶠ (x : ι) in p, pa x) (pb : α → Prop) (hpb : ∀ᶠ (y : α) in 𝓝[s] x, pb y)
    (h : ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u), ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
obtain ⟨pa, hpa, pb, hpb, h⟩ := h x hx u hu
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h_1 :
  ∀ x ∈ s,
    ∀ u ∈ 𝓤 β,
      ∃ (pa : ι → Prop),
        (∀ᶠ (x : ι) in p, pa x) ∧
          ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
pa : ι → Prop
hpa : ∀ᶠ (x : ι) in p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in 𝓝[s] x, pb y
h : ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
⟨{a | pb a}, hpb, eventually_of_mem hpa fun i hi y hy => h hi hy⟩

Premises used: setOf, Filter.eventually_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h_1 :
  ∀ x ∈ s,
    ∀ u ∈ 𝓤 β,
      ∃ (pa : ι → Prop),
        (∀ᶠ (x : ι) in p, pa x) ∧
          ∃ (pb : α → Prop), (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
pa : ι → Prop
hpa : ∀ᶠ (x : ι) in p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in 𝓝[s] x, pb y
h : ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
exact ⟨{a | pb a}, hpb, eventually_of_mem hpa fun i hi y hy => h hi hy⟩
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoLocallyUniformly F f p ↔ ∀ (x : α), TendstoUniformlyOnFilter F f p (𝓝 x)

Tactic:
simpa [← tendstoLocallyUniformlyOn_univ, ← nhdsWithin_univ] using
    @tendstoLocallyUniformlyOn_iff_filter _ _ _ _ _ F f univ p

Premises used: nhdsWithin_univ, tendstoLocallyUniformlyOn_iff_filter, tendstoLocallyUniformlyOn_univ
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hf : TendstoLocallyUniformlyOn F f p s
a : α
ha : a ∈ s
⊢ Tendsto (fun (i : ι) ↦ F i a) p (𝓝 (f a))

Tactic:
((tendstoLocallyUniformlyOn_iff_filter.mp hf) a ha).tendsto_at ?_

Premises used: TendstoUniformlyOnFilter.tendsto_at, Iff.mp, tendstoLocallyUniformlyOn_iff_filter
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hf : TendstoLocallyUniformlyOn F f p s
a : α
ha : a ∈ s
refine : 𝓟 {a} ≤ 𝓝[s] a
⊢ Tendsto (fun (i : ι) ↦ F i a) p (𝓝 (f a))

Tactic:
refine ((tendstoLocallyUniformlyOn_iff_filter.mp hf) a ha).tendsto_at ?_

Premises used: TendstoUniformlyOnFilter.tendsto_at, Iff.mp, tendstoLocallyUniformlyOn_iff_filter
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hf : TendstoLocallyUniformlyOn F f p s
a : α
ha : a ∈ s
⊢ 𝓟 {a} ≤ 𝓝[s] a

Tactic:
simpa only [Filter.principal_singleton] using pure_le_nhdsWithin ha

Premises used: pure_le_nhdsWithin, Filter.principal_singleton
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst_2 : p.NeBot
inst_3 : T2Space β
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : TendstoLocallyUniformlyOn F g p s
⊢ EqOn f g s

Tactic:
fun _a ha => tendsto_nhds_unique (hf.tendsto_at ha) (hg.tendsto_at ha)

Premises used: Set.EqOn, TendstoLocallyUniformlyOn.tendsto_at, tendsto_nhds_unique
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
⊢ ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)

Tactic:
simpa using eventually_prod_principal_iff.2 hg

Premises used: Iff.mpr, Filter.eventually_prod_principal_iff
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
⊢ ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)

Tactic:
have hg : ∀ᶠ x in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2) := by
    simpa using eventually_prod_principal_iff.2 hg
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg_1 : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)
rw :
  ∀ (hf : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β))
    (hg : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x))
    (hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)),
    ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
⊢ TendstoLocallyUniformlyOn G f p s

Tactic:
rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at hf ⊢

Premises used: tendstoLocallyUniformlyOn_iff_forall_tendsto
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg_1 : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)
⊢ ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)

Tactic:
forall₂_imp (fun x hx hf => ?_) hf

Premises used: forall₂_imp
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg_1 : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)
refine :
  ∀ (x : α) (hx : x ∈ s) (hf : Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)),
    Tendsto (fun (y : ι × α) ↦ (f y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
⊢ ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)

Tactic:
refine forall₂_imp (fun x hx hf => ?_) hf

Premises used: forall₂_imp
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf_1 : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg_1 : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)
x : α
hx : x ∈ s
hf : Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
rw :
  ∀
    (hf :
      ∀ (i : SetRel β β),
        i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, F x.1 x.2) ∈ id i)
    (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, G x.1 x.2) ∈ id i
⊢ Tendsto (fun (y : ι × α) ↦ (f y.2, G y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)

Tactic:
rw [uniformity_hasBasis_open.tendsto_right_iff] at hf ⊢

Premises used: Filter.HasBasis.tendsto_right_iff, uniformity_hasBasis_open
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf_1 : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg_1 : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)
x : α
hx : x ∈ s
hf :
  ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, F x.1 x.2) ∈ id i
⊢ ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, G x.1 x.2) ∈ id i

Tactic:
fun i hi => (hf i hi).mp ((hg.filter_mono (prod_mono_right p inf_le_right)).mono
    fun x hg hf => ((Inseparable.rfl.prod hg).mem_open_iff hi.2).1 hf)

Premises used: Filter.Eventually.filter_mono, Inseparable.rfl, inf_le_right, Filter.Eventually.mono, Filter.Eventually.mp, And.right, Iff.mp, Inseparable.prod, Filter.prod_mono_right, Inseparable.mem_open_iff
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf_1 : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg_1 : ∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (G n x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (F x.1 x.2) (G x.1 x.2)
x : α
hx : x ∈ s
hf :
  ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, F x.1 x.2) ∈ id i
⊢ ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, G x.1 x.2) ∈ id i

Tactic:
exact fun i hi => (hf i hi).mp ((hg.filter_mono (prod_mono_right p inf_le_right)).mono
    fun x hg hf => ((Inseparable.rfl.prod hg).mem_open_iff hi.2).1 hf)

Premises used: Filter.Eventually.filter_mono, Inseparable.rfl, inf_le_right, Filter.Eventually.mono, Filter.Eventually.mp, And.right, Iff.mp, Inseparable.prod, Filter.prod_mono_right, Inseparable.mem_open_iff
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
G : ι → α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ (n : ι), EqOn (F n) (G n) s
⊢ TendstoLocallyUniformlyOn G f p s

Tactic:
hf.congr_inseparable (.of_forall fun n _ hx => .of_eq (hg n hx))

Premises used: Inseparable.of_eq, Filter.Eventually.of_forall, TendstoLocallyUniformlyOn.congr_inseparable
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ x ∈ s, Inseparable (f x) (g x)
rw : ∀ᶠ (x : ι) in p, ∀ y ∈ s, Inseparable (f (x, y).2) (g (x, y).2)
⊢ ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)

Tactic:
rw [eventually_prod_principal_iff]

Premises used: Filter.eventually_prod_principal_iff
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ x ∈ s, Inseparable (f x) (g x)
⊢ ∀ᶠ (x : ι) in p, ∀ y ∈ s, Inseparable (f (x, y).2) (g (x, y).2)

Tactic:
.of_forall fun _ => hg

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ x ∈ s, Inseparable (f x) (g x)
⊢ ∀ᶠ (x : ι) in p, ∀ y ∈ s, Inseparable (f (x, y).2) (g (x, y).2)

Tactic:
exact .of_forall fun _ => hg
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : ∀ x ∈ s, Inseparable (f x) (g x)
⊢ ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)

Tactic:
have hg : ∀ᶠ x in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2) := by
    rw [eventually_prod_principal_iff]
    exact .of_forall fun _ => hg
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg_1 : ∀ x ∈ s, Inseparable (f x) (g x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)
rw :
  ∀ (hf : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β))
    (hg : ∀ x ∈ s, Inseparable (f x) (g x)) (hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)),
    ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (g y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
⊢ TendstoLocallyUniformlyOn F g p s

Tactic:
rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at hf ⊢

Premises used: tendstoLocallyUniformlyOn_iff_forall_tendsto
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg_1 : ∀ x ∈ s, Inseparable (f x) (g x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)
⊢ ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (g y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)

Tactic:
forall₂_imp (fun x hx hf => ?_) hf

Premises used: forall₂_imp
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg_1 : ∀ x ∈ s, Inseparable (f x) (g x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)
refine :
  ∀ (x : α) (hx : x ∈ s) (hf : Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)),
    Tendsto (fun (y : ι × α) ↦ (g y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
⊢ ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (g y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)

Tactic:
refine forall₂_imp (fun x hx hf => ?_) hf

Premises used: forall₂_imp
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf_1 : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg_1 : ∀ x ∈ s, Inseparable (f x) (g x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)
x : α
hx : x ∈ s
hf : Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
rw :
  ∀
    (hf :
      ∀ (i : SetRel β β),
        i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, F x.1 x.2) ∈ id i)
    (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (g x.2, F x.1 x.2) ∈ id i
⊢ Tendsto (fun (y : ι × α) ↦ (g y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)

Tactic:
rw [uniformity_hasBasis_open.tendsto_right_iff] at hf ⊢

Premises used: Filter.HasBasis.tendsto_right_iff, uniformity_hasBasis_open
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf_1 : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg_1 : ∀ x ∈ s, Inseparable (f x) (g x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)
x : α
hx : x ∈ s
hf :
  ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, F x.1 x.2) ∈ id i
⊢ ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (g x.2, F x.1 x.2) ∈ id i

Tactic:
fun i hi => (hf i hi).mp ((hg.filter_mono (prod_mono_right p inf_le_right)).mono
    fun x hg hf => ((hg.prod .rfl).mem_open_iff hi.2).1 hf)

Premises used: Filter.Eventually.filter_mono, Inseparable.rfl, inf_le_right, Filter.Eventually.mono, Filter.Eventually.mp, And.right, Iff.mp, Inseparable.prod, Filter.prod_mono_right, Inseparable.mem_open_iff
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf_1 : ∀ x ∈ s, Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β)
hg_1 : ∀ x ∈ s, Inseparable (f x) (g x)
hg : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, Inseparable (f x.2) (g x.2)
x : α
hx : x ∈ s
hf :
  ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (f x.2, F x.1 x.2) ∈ id i
⊢ ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓝[s] x, (g x.2, F x.1 x.2) ∈ id i

Tactic:
exact fun i hi => (hf i hi).mp ((hg.filter_mono (prod_mono_right p inf_le_right)).mono
    fun x hg hf => ((hg.prod .rfl).mem_open_iff hi.2).1 hf)

Premises used: Filter.Eventually.filter_mono, Inseparable.rfl, inf_le_right, Filter.Eventually.mono, Filter.Eventually.mp, And.right, Iff.mp, Inseparable.prod, Filter.prod_mono_right, Inseparable.mem_open_iff
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : TendstoLocallyUniformlyOn F f p s
hg : EqOn f g s
⊢ TendstoLocallyUniformlyOn F g p s

Tactic:
hf.congr_inseparable_right fun _ hx => .of_eq (hg hx)

Premises used: Inseparable.of_eq, TendstoLocallyUniformlyOn.congr_inseparable_right
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
G : ι → α → β
hf : TendstoLocallyUniformly F f p
hg : ∀ᶠ (n : ι) in p, ∀ (x : α), Inseparable (F n x) (G n x)
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), Membership.mem (γ := Set α) univ x → Inseparable (F n x) (G n x)

Tactic:
simpa using hg
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
G : ι → α → β
hf : TendstoLocallyUniformly F f p
hg : ∀ (n : ι) (x : α), F n x = G n x
⊢ TendstoLocallyUniformly G f p

Tactic:
hf.congr_inseparable (.of_forall fun n x => .of_eq (hg n x))

Premises used: Inseparable.of_eq, Filter.Eventually.of_forall, TendstoLocallyUniformly.congr_inseparable
-- Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
g : α → β
hf : TendstoLocallyUniformly F f p
hg : ∀ (x : α), Inseparable (f x) (g x)
⊢ ∀ (x : α), Membership.mem (γ := Set α) univ x → Inseparable (f x) (g x)

Tactic:
simpa using hg