awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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, ∀ 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:
hf.mono fun x hx y hy => (((hfg y hy).prod .rfl).mem_open_iff hi.2).mp (hx y hy)

Premises used: Inseparable.rfl, Filter.Eventually.mono, And.right, Iff.mp, 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 : α → β
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, ∀ 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:
exact hf.mono fun x hx y hy => (((hfg y hy).prod .rfl).mem_open_iff hi.2).mp (hx y hy)

Premises used: Inseparable.rfl, Filter.Eventually.mono, And.right, Iff.mp, 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 : α → β
s : Set α
p : Filter ι
g : α → β
hf : TendstoUniformlyOn F f p s
hfg : EqOn f g s
⊢ TendstoUniformlyOn F g p s

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

Premises used: Inseparable.of_eq, TendstoUniformlyOn.congr_inseparable_right
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoUniformly F f p
⊢ TendstoUniformlyOn F f p s

Tactic:
(tendstoUniformlyOn_univ.2 h).mono (subset_univ s)

Premises used: Iff.mpr, tendstoUniformlyOn_univ, Set.subset_univ, TendstoUniformlyOn.mono
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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 : γ → α
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') (𝓤 β)
⊢ TendstoUniformlyOnFilter (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p (comap g p')

Tactic:
rw [tendstoUniformlyOnFilter_iff_tendsto] at h ⊢

Premises used: tendstoUniformlyOnFilter_iff_tendsto
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
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:
h.comp (tendsto_id.prodMap tendsto_comap)

Premises used: Filter.tendsto_id, Filter.tendsto_comap, Filter.Tendsto.comp, Filter.Tendsto.prodMap
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
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:
exact h.comp (tendsto_id.prodMap tendsto_comap)

Premises used: Filter.tendsto_id, Filter.tendsto_comap, Filter.Tendsto.comp, Filter.Tendsto.prodMap
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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 : γ → α
rw :
  ∀ (h : TendstoUniformlyOnFilter F f p (𝓟 s)) (g : γ → α),
    TendstoUniformlyOnFilter (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p (𝓟 (g ⁻¹' s))
⊢ TendstoUniformlyOn (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p (g ⁻¹' s)

Tactic:
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter] at h ⊢

Premises used: tendstoUniformlyOn_iff_tendstoUniformlyOnFilter
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoUniformlyOnFilter F f p (𝓟 s)
g : γ → α
⊢ TendstoUniformlyOnFilter (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p (𝓟 (g ⁻¹' s))

Tactic:
simpa [TendstoUniformlyOn, comap_principal] using TendstoUniformlyOnFilter.comp h g

Premises used: TendstoUniformlyOn, TendstoUniformlyOnFilter.comp, Filter.comap_principal
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
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 : γ → α
rw : ∀ (h : TendstoUniformlyOnFilter F f p ⊤) (g : γ → α), TendstoUniformlyOnFilter (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p ⊤
⊢ TendstoUniformly (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p

Tactic:
rw [tendstoUniformly_iff_tendstoUniformlyOnFilter] at h ⊢

Premises used: tendstoUniformly_iff_tendstoUniformlyOnFilter
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : TendstoUniformlyOnFilter F f p ⊤
g : γ → α
⊢ TendstoUniformlyOnFilter (fun (n : ι) ↦ F n ∘ g) (f ∘ g) p ⊤

Tactic:
simpa [principal_univ, comap_principal] using h.comp g

Premises used: Filter.principal_univ, TendstoUniformlyOnFilter.comp, Filter.comap_principal
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst_1 : UniformSpace γ
g : β → γ
hg : UniformContinuous g
h : TendstoUniformlyOnFilter F f p p'
⊢ TendstoUniformlyOnFilter (fun (i : ι) ↦ g ∘ F i) (g ∘ f) p p'

Tactic:
fun _u hu => h _ (hg hu)

Premises used: Set.Mem, setOf, TendstoUniformlyOnFilter, Prod.mk, Prod.fst, Set.preimage, Prod.snd
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst_1 : UniformSpace γ
g : β → γ
hg : UniformContinuous g
h : TendstoUniformlyOn F f p s
⊢ TendstoUniformlyOn (fun (i : ι) ↦ g ∘ F i) (g ∘ f) p s

Tactic:
fun _u hu => h _ (hg hu)

Premises used: Set.Mem, setOf, Prod.mk, Prod.fst, TendstoUniformlyOn, Set.preimage, Prod.snd
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst_1 : UniformSpace γ
g : β → γ
hg : UniformContinuous g
h : TendstoUniformly F f p
⊢ TendstoUniformly (fun (i : ι) ↦ g ∘ F i) (g ∘ f) p

Tactic:
fun _u hu => h _ (hg hu)

Premises used: Set.Mem, setOf, Prod.mk, Prod.fst, TendstoUniformly, Set.preimage, Prod.snd
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : TendstoUniformlyOnFilter F f p p'
h' : TendstoUniformlyOnFilter F' f' q q'
rw :
  ∀ (h : Tendsto (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β))
    (h' : Tendsto (fun (q : ι' × α') ↦ (f' q.2, F' q.1 q.2)) (q ×ˢ q') (𝓤 β')),
    Tendsto (β := (β × β') × β × β')
      (fun (q : (ι × ι') × α × α') ↦ (Prod.map f f' q.2, Prod.map (F q.1.1) (F' q.1.2) q.2)) ((p ×ˢ q) ×ˢ p' ×ˢ q')
      (𝓤 (β × β'))
⊢ TendstoUniformlyOnFilter (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ q) (p' ×ˢ q')

Tactic:
rw [tendstoUniformlyOnFilter_iff_tendsto] at h h' ⊢

Premises used: tendstoUniformlyOnFilter_iff_tendsto
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : Tendsto (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)
h' : Tendsto (fun (q : ι' × α') ↦ (f' q.2, F' q.1 q.2)) (q ×ˢ q') (𝓤 β')
rw :
  Tendsto
    (Function.comp (β := (ι × ι') × α × α')
      ((fun (p : (β × β') × β × β') ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ fun (q : (ι × ι') × α × α') ↦
        (Prod.map f f' q.2, Prod.map (F q.1.1) (F' q.1.2) q.2))
      fun (p : (ι × α) × ι' × α') ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
    ((p ×ˢ p') ×ˢ q ×ˢ q') (𝓤 β ×ˢ 𝓤 β')
⊢ Tendsto (β := (β × β') × β × β')
    (fun (q : (ι × ι') × α × α') ↦ (Prod.map f f' q.2, Prod.map (F q.1.1) (F' q.1.2) q.2)) ((p ×ˢ q) ×ˢ p' ×ˢ q')
    (𝓤 (β × β'))

Tactic:
rw [uniformity_prod_eq_comap_prod, tendsto_comap_iff, ← map_swap4_prod, tendsto_map'_iff]

Premises used: Filter.tendsto_map'_iff, Filter.tendsto_comap_iff, Filter.map_swap4_prod, uniformity_prod_eq_comap_prod
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : Tendsto (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)
h' : Tendsto (fun (q : ι' × α') ↦ (f' q.2, F' q.1 q.2)) (q ×ˢ q') (𝓤 β')
⊢ Tendsto
    (Function.comp (β := (ι × ι') × α × α')
      ((fun (p : (β × β') × β × β') ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ fun (q : (ι × ι') × α × α') ↦
        (Prod.map f f' q.2, Prod.map (F q.1.1) (F' q.1.2) q.2))
      fun (p : (ι × α) × ι' × α') ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
    ((p ×ˢ p') ×ˢ q ×ˢ q') (𝓤 β ×ˢ 𝓤 β')

Tactic:
simpa using h.prodMap h'

Premises used: Filter.Tendsto.prodMap
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
s' : Set α'
h : TendstoUniformlyOn F f p s
h' : TendstoUniformlyOn F' f' p' s'
rw :
  ∀ (h : TendstoUniformlyOnFilter F f p (𝓟 s)) (h' : TendstoUniformlyOnFilter F' f' p' (𝓟 s')),
    TendstoUniformlyOnFilter (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (𝓟 (s ×ˢ s'))
⊢ TendstoUniformlyOn (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (s ×ˢ s')

Tactic:
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter] at h h' ⊢

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 ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
s' : Set α'
h : TendstoUniformlyOnFilter F f p (𝓟 s)
h' : TendstoUniformlyOnFilter F' f' p' (𝓟 s')
⊢ TendstoUniformlyOnFilter (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (𝓟 (s ×ˢ s'))

Tactic:
simpa only [prod_principal_principal] using h.prodMap h'

Premises used: Filter.prod_principal_principal, TendstoUniformlyOnFilter.prodMap
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
h : TendstoUniformly F f p
h' : TendstoUniformly F' f' p'
rw :
  ∀ (h : TendstoUniformlyOn F f p univ) (h' : TendstoUniformlyOn F' f' p' univ),
    TendstoUniformlyOn (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p')
      (SProd.sprod (α := Set α) (β := Set α') univ univ)
⊢ TendstoUniformly (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p')

Tactic:
rw [← tendstoUniformlyOn_univ, ← univ_prod_univ] at *

Premises used: tendstoUniformlyOn_univ, Set.univ_prod_univ
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
h : TendstoUniformlyOn F f p univ
h' : TendstoUniformlyOn F' f' p' univ
⊢ TendstoUniformlyOn (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p')
    (SProd.sprod (α := Set α) (β := Set α') univ univ)

Tactic:
h.prodMap h'

Premises used: TendstoUniformlyOn.prodMap
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
h : TendstoUniformlyOn F f p univ
h' : TendstoUniformlyOn F' f' p' univ
⊢ TendstoUniformlyOn (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p')
    (SProd.sprod (α := Set α) (β := Set α') univ univ)

Tactic:
exact h.prodMap h'

Premises used: TendstoUniformlyOn.prodMap
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
ι' : Type u_5
β' : Type u_6
inst_1 : UniformSpace β'
F' : ι' → α → β'
f' : α → β'
q : Filter ι'
h : TendstoUniformlyOnFilter F f p p'
h' : TendstoUniformlyOnFilter F' f' q p'
⊢ TendstoUniformlyOnFilter (β := β × β') (fun (i : ι × ι') (a : α) ↦ (F i.1 a, F' i.2 a)) (fun (a : α) ↦ (f a, f' a))
    (p ×ˢ q) p'

Tactic:
fun u hu => ((h.prodMap h') u hu).diag_of_prod_right

Premises used: Set.Mem, Filter.Eventually.diag_of_prod_right, TendstoUniformlyOnFilter, Prod.map, TendstoUniformlyOnFilter.prodMap
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
ι' : Type u_5
β' : Type u_6
inst_1 : UniformSpace β'
F' : ι' → α → β'
f' : α → β'
p' : Filter ι'
h : TendstoUniformlyOn F f p s
h' : TendstoUniformlyOn F' f' p' s
⊢ TendstoUniformlyOn (β := β × β') (fun (i : ι × ι') (a : α) ↦ (F i.1 a, F' i.2 a)) (fun (a : α) ↦ (f a, f' a))
    (p ×ˢ p') s

Tactic:
(congr_arg _ s.inter_self).mp ((h.prodMap h').comp fun a => (a, a))

Premises used: TendstoUniformlyOn.comp, Set.inter_self, Eq.mp, Prod.mk, congr_arg, TendstoUniformlyOn.prodMap
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
ι' : Type u_5
β' : Type u_6
inst_1 : UniformSpace β'
F' : ι' → α → β'
f' : α → β'
p' : Filter ι'
h : TendstoUniformly F f p
h' : TendstoUniformly F' f' p'
⊢ TendstoUniformly (β := β × β') (fun (i : ι × ι') (a : α) ↦ (F i.1 a, F' i.2 a)) (fun (a : α) ↦ (f a, f' a)) (p ×ˢ p')

Tactic:
(h.prodMap h').comp fun a => (a, a)

Premises used: Prod.mk, Prod.map, TendstoUniformly.comp, TendstoUniformly.prodMap
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
c : β
simp_rw : Tendsto (Prod.mk c ∘ ↿F) (p ×ˢ p') (𝓤 β) ↔ TendstoUniformlyOnFilter F (fun (x : α) ↦ c) p p'
⊢ Tendsto (↿F) (p ×ˢ p') (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun (x : α) ↦ c) p p'

Tactic:
simp_rw [nhds_eq_comap_uniformity, tendsto_comap_iff]

Premises used: Filter.tendsto_comap_iff, nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
c : β
⊢ Tendsto (Prod.mk c ∘ ↿F) (p ×ˢ p') (𝓤 β) ↔ TendstoUniformlyOnFilter F (fun (x : α) ↦ c) p p'

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
c : β
rw : Tendsto (↿F) (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun (x : α) ↦ c) p (𝓟 s)
⊢ Tendsto (↿F) (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOn F (fun (x : α) ↦ c) p s

Tactic:
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter]

Premises used: tendstoUniformlyOn_iff_tendstoUniformlyOnFilter
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
c : β
⊢ Tendsto (↿F) (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun (x : α) ↦ c) p (𝓟 s)

Tactic:
tendsto_prod_filter_iff

Premises used: tendsto_prod_filter_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
c : β
⊢ Tendsto (↿F) (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun (x : α) ↦ c) p (𝓟 s)

Tactic:
exact tendsto_prod_filter_iff

Premises used: tendsto_prod_filter_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
p : Filter ι
c : β
rw : Tendsto (↿F) (SProd.sprod (β := Filter α) p ⊤) (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun (x : α) ↦ c) p ⊤
⊢ Tendsto (↿F) (SProd.sprod (β := Filter α) p ⊤) (𝓝 c) ↔ TendstoUniformly F (fun (x : α) ↦ c) p

Tactic:
rw [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 : ι → α → β
p : Filter ι
c : β
⊢ Tendsto (↿F) (SProd.sprod (β := Filter α) p ⊤) (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun (x : α) ↦ c) p ⊤

Tactic:
tendsto_prod_filter_iff

Premises used: tendsto_prod_filter_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
p : Filter ι
c : β
⊢ Tendsto (↿F) (SProd.sprod (β := Filter α) p ⊤) (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun (x : α) ↦ c) p ⊤

Tactic:
exact tendsto_prod_filter_iff

Premises used: tendsto_prod_filter_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
u : Set (β × β)
h : u ∈ 𝓤 β
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), Membership.mem (γ := Set α) ∅ x → (f x, F n x) ∈ u

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
simp_rw :
  (∀ s ∈ 𝓤 β, (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) ⁻¹' s ∈ SProd.sprod (β := Filter α) p (𝓟 {x})) ↔
    ∀ s ∈ 𝓤 β, (fun (x_1 : ι) ↦ (f x, F x_1 x)) ⁻¹' s ∈ p
⊢ TendstoUniformlyOn F f p {x} ↔ Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))

Tactic:
simp_rw [tendstoUniformlyOn_iff_tendsto, Uniform.tendsto_nhds_right, tendsto_def]

Premises used: Filter.tendsto_def, tendstoUniformlyOn_iff_tendsto, Uniform.tendsto_nhds_right
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
u : Set (β × β)
h : u ∈ 𝓤 β
⊢ (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) ⁻¹' u ∈ SProd.sprod (β := Filter α) p (𝓟 {x}) ↔
    (fun (x_1 : ι) ↦ (f x, F x_1 x)) ⁻¹' u ∈ p

Tactic:
simp [preimage]

Premises used: Set.preimage
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
⊢ (∀ s ∈ 𝓤 β, (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) ⁻¹' s ∈ SProd.sprod (β := Filter α) p (𝓟 {x})) ↔
    ∀ s ∈ 𝓤 β, (fun (x_1 : ι) ↦ (f x, F x_1 x)) ⁻¹' s ∈ p

Tactic:
exact forall₂_congr fun u _ => by simp [preimage]

Premises used: forall₂_congr
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
p : Filter ι
g : ι → β
b : β
hg : Tendsto g p (𝓝 b)
p' : Filter α
⊢ TendstoUniformlyOnFilter.{u_1, u_2, u_4} (β := β) (fun (n : ι) (x : α) ↦ g n) (fun (x : α) ↦ b) p p'

Tactic:
simpa only [nhds_eq_comap_uniformity, tendsto_comap_iff] using hg.comp (tendsto_fst (g := p'))

Premises used: Filter.tendsto_comap_iff, nhds_eq_comap_uniformity, Filter.Tendsto.comp, Filter.tendsto_fst
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
p : Filter ι
g : ι → β
b : β
hg : Tendsto g p (𝓝 b)
s : Set α
⊢ TendstoUniformlyOn.{u_1, u_2, u_4} (β := β) (fun (n : ι) (x : α) ↦ g n) (fun (x : α) ↦ b) p s

Tactic:
tendstoUniformlyOn_iff_tendstoUniformlyOnFilter.mpr (hg.tendstoUniformlyOnFilter_const (𝓟 s))

Premises used: Iff.mpr, Filter.Tendsto.tendstoUniformlyOnFilter_const, tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, Filter.principal
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
p : Filter ι
g : ι → β
b : β
hg : Tendsto g p (𝓝 b)
⊢ TendstoUniformly.{u_1, u_2, u_4} (β := β) (fun (n : ι) (x : α) ↦ g n) (fun (x : α) ↦ b) p

Tactic:
tendstoUniformly_iff_tendstoUniformlyOnFilter.mpr (hg.tendstoUniformlyOnFilter_const _)

Premises used: tendstoUniformly_iff_tendstoUniformlyOnFilter, Iff.mpr, Filter.Tendsto.tendstoUniformlyOnFilter_const
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
x : α
inst_1 : UniformSpace α
inst_2 : UniformSpace γ
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : (q : α × β) → (α × β) × α × β := fun (q : α × β) ↦ ((x, q.2), q)
rw : Tendsto (fun (q : α × β) ↦ (F x q.2, F q.1 q.2)) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
⊢ TendstoUniformlyOn F (F x) (𝓝[U] x) V

Tactic:
rw [tendstoUniformlyOn_iff_tendsto]

Premises used: tendstoUniformlyOn_iff_tendsto
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
x : α
inst_1 : UniformSpace α
inst_2 : UniformSpace γ
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : (q : α × β) → (α × β) × α × β := fun (q : α × β) ↦ ((x, q.2), q)
change : Tendsto (Prod.map ↿F ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
⊢ Tendsto (fun (q : α × β) ↦ (F x q.2, F q.1 q.2)) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)

Tactic:
change Tendsto (Prod.map ↿F ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)

Premises used: SProd.sprod, nhdsWithin, uniformity, Function.comp, Prod.map, Filter.Tendsto, Function.HasUncurry.uncurry, Filter.principal
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
x : α
inst_1 : UniformSpace α
inst_2 : UniformSpace γ
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : (q : α × β) → (α × β) × α × β := fun (q : α × β) ↦ ((x, q.2), q)
simp : Tendsto (Prod.map ↿F ↿F ∘ φ) (comap Prod.fst (𝓝 x) ⊓ 𝓟 (Prod.fst ⁻¹' U ∩ Prod.snd ⁻¹' V)) (𝓤 γ)
⊢ Tendsto (Prod.map ↿F ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)

Tactic:
simp only [nhdsWithin, Filter.prod_eq_inf, comap_inf, inf_assoc, comap_principal, inf_principal]

Premises used: Filter.inf_principal, nhdsWithin, Filter.prod_eq_inf, Filter.comap_inf, Filter.comap_principal, inf_assoc