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 : ι → α → β
s : Set α
p : Filter ι
γ : Type u_5
hf : UniformCauchySeqOnFilter F p (𝓟 s)
g : γ → α
⊢ UniformCauchySeqOnFilter.{u_5, u_2, u_4} (β := β) (fun (n : ι) ↦ F n ∘ g) p (𝓟 (g ⁻¹' s))

Tactic:
simpa only [UniformCauchySeqOn, comap_principal] using hf.comp g

Premises used: UniformCauchySeqOnFilter.comp, UniformCauchySeqOn, Filter.comap_principal
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
inst_1 : UniformSpace γ
g : β → γ
hg : UniformContinuous g
hf : UniformCauchySeqOn F p s
⊢ UniformCauchySeqOn.{u_1, u_3, u_4} (β := γ) (fun (n : ι) ↦ g ∘ F n) p s

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

Premises used: Set.Mem, setOf, Prod.mk, Prod.fst, Set.preimage, UniformCauchySeqOn, Prod.snd
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
hu : Membership.mem (γ := Filter ((β × β') × β × β')) (𝓤 (β × β')) u
⊢ ∃ t₁ ∈ 𝓤 β,
    ∃ t₂ ∈ 𝓤 β', t₁ ×ˢ t₂ ⊆ (fun (p : Prod.{u_2, u_7} (β × β) (β' × β')) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u

Tactic:
rw [uniformity_prod_eq_prod, mem_map, mem_prod_iff] at hu

Premises used: uniformity_prod_eq_prod, Filter.mem_prod_iff, Filter.mem_map
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
hu :
  ∃ t₁ ∈ 𝓤 β,
    ∃ t₂ ∈ 𝓤 β', t₁ ×ˢ t₂ ⊆ (fun (p : Prod.{u_2, u_7} (β × β) (β' × β')) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u
obtain :
  ∀ (v : Set (β × β)) (hv : v ∈ 𝓤 β) (w : Set (β' × β')) (hw : w ∈ 𝓤 β')
    (hvw : v ×ˢ w ⊆ (fun (p : Prod.{u_2, u_7} (β × β) (β' × β')) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u),
    ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
      ∀ x ∈ s ×ˢ s',
        ((fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) m.1 x, (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) m.2 x) ∈ u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ x ∈ s ×ˢ s',
      ((fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) m.1 x, (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) m.2 x) ∈ u

Tactic:
obtain ⟨v, hv, w, hw, hvw⟩ := hu
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : v ×ˢ w ⊆ (fun (p : Prod.{u_2, u_7} (β × β) (β' × β')) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u
simp_rw :
  ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F m.1.1 a, F' m.1.2 b), F m.2.1 a, F' m.2.2 b) ∈ u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ x ∈ s ×ˢ s',
      ((fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) m.1 x, (fun (i : ι × ι') ↦ Prod.map (F i.1) (F' i.2)) m.2 x) ∈ u

Tactic:
simp_rw [mem_prod, and_imp, Prod.forall, Prod.map_apply]

Premises used: and_imp, Set.mem_prod, Prod.map_apply, Prod.forall
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : v ×ˢ w ⊆ (fun (p : Prod.{u_2, u_7} (β × β) (β' × β')) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u
⊢ (fun (p : Prod.{u_2, u_7} (β × β) (β' × β')) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u

Tactic:
rw [← Set.image_subset_iff] at hvw

Premises used: Set.image_subset_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : (fun (p : Prod.{u_2, u_7} (β × β) (β' × β')) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u
apply :
  ∀ (x : (ι × ι') × ι × ι'),
    ((∀ x_1 ∈ s, (F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 x_1, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.2 x_1) ∈ v) ∧
        ∀ x_1 ∈ s', (F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 x_1, F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.2 x_1) ∈ w) →
      ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F x.1.1 a, F' x.1.2 b), F x.2.1 a, F' x.2.2 b) ∈ u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F m.1.1 a, F' m.1.2 b), F m.2.1 a, F' m.2.2 b) ∈ u

Tactic:
apply (tendsto_swap4_prod.eventually ((h v hv).prod_mk (h' w hw))).mono

Premises used: Filter.Eventually.mono, Filter.Eventually.prod_mk, Filter.tendsto_swap4_prod, Filter.Tendsto.eventually
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : (fun (p : Prod.{u_2, u_7} (β × β) (β' × β')) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u
x : (ι × ι') × ι × ι'
hx :
  (∀ x_1 ∈ s, (F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 x_1, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.2 x_1) ∈ v) ∧
    ∀ x_1 ∈ s', (F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 x_1, F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.2 x_1) ∈ w
a : α
b : α'
ha : a ∈ s
hb : b ∈ s'
⊢ ((F x.1.1 a, F' x.1.2 b), F x.2.1 a, F' x.2.2 b) ∈ u

Tactic:
hvw ⟨_, mk_mem_prod (hx.1 a ha) (hx.2 b hb), rfl⟩

Premises used: Set.Mem, And.right, And.left, And.intro, Exists.intro, Set.mk_mem_prod, rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst_1 : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : (fun (p : Prod.{u_2, u_7} (β × β) (β' × β')) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u
x : (ι × ι') × ι × ι'
hx :
  (∀ x_1 ∈ s, (F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 x_1, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.2 x_1) ∈ v) ∧
    ∀ x_1 ∈ s', (F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 x_1, F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.2 x_1) ∈ w
a : α
b : α'
ha : a ∈ s
hb : b ∈ s'
⊢ ((F x.1.1 a, F' x.1.2 b), F x.2.1 a, F' x.2.2 b) ∈ u

Tactic:
exact hvw ⟨_, mk_mem_prod (hx.1 a ha) (hx.2 b hb), rfl⟩

Premises used: And.right, And.left, And.intro, Exists.intro, Set.mk_mem_prod, rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_5
β' : Type u_6
inst_1 : UniformSpace β'
F' : ι' → α → β'
p' : Filter ι'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s
⊢ UniformCauchySeqOn (β := β × β') (fun (i : ι × ι') (a : α) ↦ (F i.1 a, F' i.2 a)) (p ×ˢ p') s

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

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

Tactic:
fun u hu =>
  have hh : Tendsto (fun x : ι => (x, x)) p (p ×ˢ p) := tendsto_diag
  (hh.prodMap hh).eventually ((h.prod h') u hu)

Premises used: UniformCauchySeqOn.prod, Set.Mem, Filter.tendsto_diag, Filter.Tendsto.eventually, UniformCauchySeqOn, Filter.Tendsto.prodMap
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
simp : Tendsto (fun (p : ι × ι) ↦ (F p.1 x, F p.2 x)) (p ×ˢ p) (𝓤 β)
⊢ Cauchy.{u_2} (α := β) (map (fun (i : ι) ↦ F i x) p)

Tactic:
simp only [cauchy_map_iff, hp, true_and]

Premises used: cauchy_map_iff, true_and
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
x : α
p_1 : Filter ι
hp_1 : p_1.NeBot
hf : UniformCauchySeqOn F p_1 s
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
p : ι × ι
hp : ∀ x ∈ s, (F p.1 x, F p.2 x) ∈ u
⊢ Membership.mem (γ := Set (ι × ι)) ((fun (p : ι × ι) ↦ (F p.1 x, F p.2 x)) ⁻¹' u) p

Tactic:
hp x hx

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
h :
  ∀ (a : ι × ι),
    Membership.mem (γ := Set (ι × ι))
      {x_1 : ι × ι |
        Membership.mem (γ := Set (ι × ι)) {x : ι × ι | (fun (m : ι × ι) ↦ ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) x} x_1 →
          Membership.mem (γ := Set (ι × ι)) ((fun (p : ι × ι) ↦ (F p.1 x, F p.2 x)) ⁻¹' u) x_1}
      a
h₁ h₂ :
  ∀ (p : ι × ι) (hp : ∀ x ∈ s, (F p.1 x, F p.2 x) ∈ u),
    Membership.mem (γ := Set (ι × ι)) ((fun (p : ι × ι) ↦ (F p.1 x, F p.2 x)) ⁻¹' u) p
⊢ (fun (p : ι × ι) ↦ (F p.1 x, F p.2 x)) ⁻¹' u ∈ p ×ˢ p

Tactic:
filter_upwards [hf u hu] with p hp using hp x hx
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
x : α
inst_1 : Nonempty ι
inst_2 : SemilatticeSup ι
hf : UniformCauchySeqOn F atTop s
hx : x ∈ s
⊢ CauchySeq.{u_2, u_4} (α := β) fun (i : ι) ↦ F i x

Tactic:
hf.cauchy_map (hp := atTop_neBot) hx

Premises used: UniformCauchySeqOn.cauchy_map, CauchySeq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
inst_1 : l.IsCountablyGenerated
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun (n : ℕ) ↦ F (u n)) f atTop s
rw : ∀ (x : ℕ → ι × α), Tendsto x atTop (l ×ˢ 𝓟 s) → Tendsto ((fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) ∘ x) atTop (𝓤 β)
⊢ TendstoUniformlyOn F f l s

Tactic:
rw [tendstoUniformlyOn_iff_tendsto, tendsto_iff_seq_tendsto]

Premises used: tendstoUniformlyOn_iff_tendsto, Filter.tendsto_iff_seq_tendsto
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
inst_1 : l.IsCountablyGenerated
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun (n : ℕ) ↦ F (u n)) f atTop s
u : ℕ → ι × α
hu : Tendsto u atTop (l ×ˢ 𝓟 s)
⊢ Tendsto (fun (n : ℕ) ↦ (u n).1) atTop l ∧ Tendsto (fun (n : ℕ) ↦ (u n).2) atTop (𝓟 s)

Tactic:
rw [tendsto_prod_iff'] at hu

Premises used: Filter.tendsto_prod_iff'
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
inst_1 : l.IsCountablyGenerated
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun (n : ℕ) ↦ F (u n)) f atTop s
u : ℕ → ι × α
hu : Tendsto (fun (n : ℕ) ↦ (u n).1) atTop l ∧ Tendsto (fun (n : ℕ) ↦ (u n).2) atTop (𝓟 s)
⊢ TendstoUniformlyOn (fun (n : ℕ) ↦ F (u n).1) f atTop s

Tactic:
specialize h (fun n => (u n).fst) hu.1

Premises used: Prod.fst, And.left
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
inst_1 : l.IsCountablyGenerated
u : ℕ → ι × α
hu : Tendsto (fun (n : ℕ) ↦ (u n).1) atTop l ∧ Tendsto (fun (n : ℕ) ↦ (u n).2) atTop (𝓟 s)
h : TendstoUniformlyOn (fun (n : ℕ) ↦ F (u n).1) f atTop s
⊢ Tendsto (fun (q : ℕ × α) ↦ (f q.2, F (u q.1).1 q.2)) (SProd.sprod (α := Filter ℕ) atTop (𝓟 s)) (𝓤 β)

Tactic:
rw [tendstoUniformlyOn_iff_tendsto] at h

Premises used: tendstoUniformlyOn_iff_tendsto
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
inst_1 : l.IsCountablyGenerated
u : ℕ → ι × α
hu : Tendsto (fun (n : ℕ) ↦ (u n).1) atTop l ∧ Tendsto (fun (n : ℕ) ↦ (u n).2) atTop (𝓟 s)
h : Tendsto (fun (q : ℕ × α) ↦ (f q.2, F (u q.1).1 q.2)) (SProd.sprod (α := Filter ℕ) atTop (𝓟 s)) (𝓤 β)
⊢ Tendsto ((fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) ∘ u) atTop (𝓤 β)

Tactic:
h.comp (tendsto_id.prodMk hu.2)

Premises used: Filter.tendsto_id, And.right, Filter.Tendsto.prodMk, Filter.Tendsto.comp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
inst_1 : l.IsCountablyGenerated
u : ℕ → ι × α
hu : Tendsto (fun (n : ℕ) ↦ (u n).1) atTop l ∧ Tendsto (fun (n : ℕ) ↦ (u n).2) atTop (𝓟 s)
h : Tendsto (fun (q : ℕ × α) ↦ (f q.2, F (u q.1).1 q.2)) (SProd.sprod (α := Filter ℕ) atTop (𝓟 s)) (𝓤 β)
⊢ Tendsto ((fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) ∘ u) atTop (𝓤 β)

Tactic:
exact h.comp (tendsto_id.prodMk hu.2)

Premises used: Filter.tendsto_id, And.right, Filter.Tendsto.prodMk, Filter.Tendsto.comp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
h : TendstoUniformlyOn F f l s
u : ℕ → ι
hu : Tendsto u atTop l
rw :
  ∀ (h : Tendsto (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) (l ×ˢ 𝓟 s) (𝓤 β)) (u : ℕ → ι) (hu : Tendsto u atTop l),
    Tendsto (fun (q : ℕ × α) ↦ (f q.2, F (u q.1) q.2)) (SProd.sprod (α := Filter ℕ) atTop (𝓟 s)) (𝓤 β)
⊢ TendstoUniformlyOn (fun (n : ℕ) ↦ F (u n)) f atTop s

Tactic:
rw [tendstoUniformlyOn_iff_tendsto] at h ⊢

Premises used: tendstoUniformlyOn_iff_tendsto
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
h : Tendsto (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) (l ×ˢ 𝓟 s) (𝓤 β)
u : ℕ → ι
hu : Tendsto u atTop l
⊢ Tendsto (fun (q : ℕ × α) ↦ (f q.2, F (u q.1) q.2)) (SProd.sprod (α := Filter ℕ) atTop (𝓟 s)) (𝓤 β)

Tactic:
h.comp ((hu.comp tendsto_fst).prodMk tendsto_snd)

Premises used: Filter.Tendsto.prodMk, Filter.Tendsto.comp, Filter.tendsto_snd, Filter.tendsto_fst
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
h : Tendsto (fun (q : ι × α) ↦ (f q.2, F q.1 q.2)) (l ×ˢ 𝓟 s) (𝓤 β)
u : ℕ → ι
hu : Tendsto u atTop l
⊢ Tendsto (fun (q : ℕ × α) ↦ (f q.2, F (u q.1) q.2)) (SProd.sprod (α := Filter ℕ) atTop (𝓟 s)) (𝓤 β)

Tactic:
exact h.comp ((hu.comp tendsto_fst).prodMk tendsto_snd)

Premises used: Filter.Tendsto.prodMk, Filter.Tendsto.comp, Filter.tendsto_snd, Filter.tendsto_fst
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
inst_1 : l.IsCountablyGenerated
⊢ TendstoUniformlyOn F f l s ↔ ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun (n : ℕ) ↦ F (u n)) f atTop s

Tactic:
⟨TendstoUniformlyOn.seq_tendstoUniformlyOn, tendstoUniformlyOn_of_seq_tendstoUniformlyOn⟩

Premises used: TendstoUniformlyOn.seq_tendstoUniformlyOn, tendstoUniformlyOn_of_seq_tendstoUniformlyOn, Iff.intro
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
l : Filter ι
inst_1 : l.IsCountablyGenerated
simp_rw :
  TendstoUniformlyOn F f l univ ↔
    ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun (n : ℕ) ↦ F (u n)) f atTop univ
⊢ TendstoUniformly F f l ↔ ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformly (fun (n : ℕ) ↦ F (u n)) f atTop

Tactic:
simp_rw [← 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 : α → β
l : Filter ι
inst_1 : l.IsCountablyGenerated
⊢ TendstoUniformlyOn F f l univ ↔
    ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun (n : ℕ) ↦ F (u n)) f atTop univ

Tactic:
tendstoUniformlyOn_iff_seq_tendstoUniformlyOn

Premises used: tendstoUniformlyOn_iff_seq_tendstoUniformlyOn
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
l : Filter ι
inst_1 : l.IsCountablyGenerated
⊢ TendstoUniformlyOn F f l univ ↔
    ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun (n : ℕ) ↦ F (u n)) f atTop univ

Tactic:
exact tendstoUniformlyOn_iff_seq_tendstoUniformlyOn

Premises used: tendstoUniformlyOn_iff_seq_tendstoUniformlyOn
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst_1 : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
rw : Tendsto (fun (x : α) ↦ (f x, ℓ)) p' (𝓤 β)
⊢ Tendsto f p' (𝓝 ℓ)

Tactic:
rw [tendsto_nhds_left]

Premises used: Uniform.tendsto_nhds_left
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst_1 : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
rw : ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x : α) ↦ (f x, ℓ)) p') s

Tactic:
rw [mem_map, Set.preimage, ← eventually_iff]

Premises used: Filter.eventually_iff, Set.preimage, Filter.mem_map
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst_1 : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
obtain : ∀ (t : Set (β × β)) (ht : t ∈ 𝓤 β) (hts : SetRel.comp t (SetRel.comp t t) ⊆ s), ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Tactic:
obtain ⟨t, ht, hts⟩ := comp3_mem_uniformity hs

Premises used: comp3_mem_uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst_1 : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : SetRel.comp t (SetRel.comp t t) ⊆ s
⊢ ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t

Tactic:
have p1 : ∀ᶠ i in p, (L i, ℓ) ∈ t := tendsto_nhds_left.mp h3 ht
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst_1 : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2_1 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : SetRel.comp t (SetRel.comp t t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
i : ι
h2 : Tendsto (F i) p' (𝓝 (L i))
⊢ ∀ᶠ (x : α) in p', (F i x, L i) ∈ t

Tactic:
tendsto_nhds_left.mp h2 ht

Premises used: Set.Mem, Filter.Eventually, setOf, Set.preimage, Iff.mp, Uniform.tendsto_nhds_left
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst_1 : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : SetRel.comp t (SetRel.comp t t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ Tendsto (F i) p' (𝓝 (L i))) x} x →
          Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ ∀ᶠ (x : α) in p', (F i x, L i) ∈ t) x} x}
      a
h₁ h₂ : ∀ (i : ι) (h2 : Tendsto (F i) p' (𝓝 (L i))), ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
⊢ ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t

Tactic:
filter_upwards [h2] with i h2 using tendsto_nhds_left.mp h2 ht
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst_1 : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : SetRel.comp t (SetRel.comp t t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
⊢ ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t

Tactic:
have p2 : ∀ᶠ i in p, ∀ᶠ x in p', (F i x, L i) ∈ t := by
    filter_upwards [h2] with i h2 using tendsto_nhds_left.mp h2 ht
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst_1 : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : SetRel.comp t (SetRel.comp t t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
p2 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
⊢ ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (f x, F i x) ∈ t

Tactic:
have p3 : ∀ᶠ i in p, ∀ᶠ x in p', (f x, F i x) ∈ t := (h1 t ht).curry
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst_1 : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : SetRel.comp t (SetRel.comp t t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
p2 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
p3 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (f x, F i x) ∈ t
obtain :
  ∀ (i : ι) (p4 : (L i, ℓ) ∈ t) (p5 : ∀ᶠ (x : α) in p', (F i x, L i) ∈ t) (p6 : ∀ᶠ (x : α) in p', (f x, F i x) ∈ t),
    ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Tactic:
obtain ⟨i, p4, p5, p6⟩ := (p1.and (p2.and p3)).exists

Premises used: Filter.Eventually.and, Filter.Eventually.exists