awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ Tendsto (Prod.map ↿F ↿F ∘ φ) (comap Prod.fst (𝓝 x) ⊓ 𝓟 (Prod.fst ⁻¹' U ∩ Prod.snd ⁻¹' V)) (𝓤 γ)

Tactic:
Tendsto.comp hF
    (Tendsto.inf ?_ <| tendsto_principal_principal.2 fun x hx => ⟨⟨hU, hx.2⟩, hx⟩)

Premises used: Iff.mpr, And.right, And.intro, Filter.Tendsto.comp, Filter.Tendsto.inf, Filter.tendsto_principal_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)
refine : Tendsto φ (comap Prod.fst (𝓝 x)) (𝓤 (α × β))
⊢ Tendsto (Prod.map ↿F ↿F ∘ φ) (comap Prod.fst (𝓝 x) ⊓ 𝓟 (Prod.fst ⁻¹' U ∩ Prod.snd ⁻¹' V)) (𝓤 γ)

Tactic:
refine Tendsto.comp hF
    (Tendsto.inf ?_ <| tendsto_principal_principal.2 fun x hx => ⟨⟨hU, hx.2⟩, hx⟩)

Premises used: Iff.mpr, And.intro, Filter.Tendsto.comp, Filter.Tendsto.inf, Filter.tendsto_principal_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 ((fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ φ) (comap (Prod.mk x ∘ Prod.fst) (𝓤 α))
    (𝓤 α ×ˢ 𝓤 β)
⊢ Tendsto φ (comap Prod.fst (𝓝 x)) (𝓤 (α × β))

Tactic:
simp only [uniformity_prod_eq_comap_prod, tendsto_comap_iff,
    nhds_eq_comap_uniformity, comap_comap]

Premises used: Filter.tendsto_comap_iff, Filter.comap_comap, uniformity_prod_eq_comap_prod, nhds_eq_comap_uniformity
-- 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)
⊢ Tendsto ((fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ φ) (comap (Prod.mk x ∘ Prod.fst) (𝓤 α))
    (𝓤 α ×ˢ 𝓤 β)

Tactic:
tendsto_comap.prodMk (tendsto_diag_uniformity _ _)

Premises used: tendsto_diag_uniformity, Filter.tendsto_comap, Filter.Tendsto.prodMk
-- 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)
⊢ Tendsto ((fun (p : (α × β) × α × β) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ φ) (comap (Prod.mk x ∘ Prod.fst) (𝓤 α))
    (𝓤 α ×ˢ 𝓤 β)

Tactic:
exact tendsto_comap.prodMk (tendsto_diag_uniformity _ _)

Premises used: tendsto_diag_uniformity, Filter.tendsto_comap, Filter.Tendsto.prodMk
-- 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 α
hU : U ∈ 𝓝 x
F : α → β → γ
hF : UniformContinuousOn (↿F) (SProd.sprod (β := Set β) U univ)
⊢ TendstoUniformly F (F x) (𝓝 x)

Tactic:
simpa only [tendstoUniformlyOn_univ, nhdsWithin_eq_nhds.2 hU]
    using hF.tendstoUniformlyOn (mem_of_mem_nhds hU)

Premises used: Iff.mpr, tendstoUniformlyOn_univ, nhdsWithin_eq_nhds, mem_of_mem_nhds, UniformContinuousOn.tendstoUniformlyOn
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
x : α
inst_1 : UniformSpace α
inst_2 : UniformSpace γ
f : α → β → γ
h : UniformContinuous₂ f
rwa : UniformContinuousOn (↿f) univ
rwa₁ rwa₂ rwa₃ rwa₄ : UniformContinuous ↿f
⊢ UniformContinuousOn (↿f) (SProd.sprod (α := Set α) (β := Set β) univ univ)

Tactic:
rwa [univ_prod_univ, uniformContinuousOn_univ]

Premises used: uniformContinuousOn_univ, Set.univ_prod_univ
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
l' : Filter α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
rw :
  Tendsto (fun (q : X × α) ↦ (f q.2, F q.1 q.2)) (l ×ˢ l') (𝓤 β) ↔
    ∀ (i : ιβ), pβ i → ∀ᶠ (n : X × α) in l ×ˢ l', (f n.2, F n.1 n.2) ∈ sβ i
rw₁ rw₂ :
  (∀ (i : ιβ), pβ i → ∀ᶠ (x : X × α) in l ×ˢ l', (f x.2, F x.1 x.2) ∈ sβ i) ↔
    ∀ (i : ιβ), pβ i → ∀ᶠ (n : X × α) in l ×ˢ l', (f n.2, F n.1 n.2) ∈ sβ i
⊢ TendstoUniformlyOnFilter F f l l' ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X × α) in l ×ˢ l', (f n.2, F n.1 n.2) ∈ sβ i

Tactic:
rw [tendstoUniformlyOnFilter_iff_tendsto, hβ.tendsto_right_iff]

Premises used: tendstoUniformlyOnFilter_iff_tendsto, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
X : Type u_5
ιX : Type u_6
ια : Type u_7
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
l' : Filter α
pX : ιX → Prop
sX : ιX → Set X
pα : ια → Prop
sα : ια → Set α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hl : l.HasBasis pX sX
hl' : l'.HasBasis pα sα
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformlyOnFilter F f l l' ↔
    ∀ (i : ιβ), pβ i → ∃ (j : ιX) (k : ια), (pX j ∧ pα k) ∧ ∀ (x : X) (a : α), x ∈ sX j → a ∈ sα k → (f a, F x a) ∈ sβ i

Tactic:
simp [hβ.tendstoUniformlyOnFilter_iff_of_uniformity, (hl.prod hl').eventually_iff]

Premises used: Filter.HasBasis.eventually_iff, Filter.HasBasis.tendstoUniformlyOnFilter_iff_of_uniformity, Filter.HasBasis.prod
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
s : Set α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
simp_rw :
  Tendsto (fun (q : X × α) ↦ (f q.2, F q.1 q.2)) (l ×ˢ 𝓟 s) (𝓤 β) ↔
    ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ x ∈ s, (f x, F n x) ∈ sβ i
simp_rw₁ :
  (∀ (i : ιβ), pβ i → ∀ᶠ (x : X × α) in l ×ˢ 𝓟 s, (f x.2, F x.1 x.2) ∈ sβ i) ↔
    ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ x ∈ s, (f x, F n x) ∈ sβ i
⊢ TendstoUniformlyOn F f l s ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ x ∈ s, (f x, F n x) ∈ sβ i

Tactic:
simp_rw [tendstoUniformlyOn_iff_tendsto, hβ.tendsto_right_iff, eventually_prod_principal_iff]

Premises used: tendstoUniformlyOn_iff_tendsto, Filter.eventually_prod_principal_iff, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
X : Type u_5
ιX : Type u_6
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
s : Set α
pX : ιX → Prop
sX : ιX → Set X
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hl : l.HasBasis pX sX
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformlyOn F f l s ↔ ∀ (i : ιβ), pβ i → ∃ (j : ιX), pX j ∧ ∀ ⦃x : X⦄, x ∈ sX j → ∀ a ∈ s, (f a, F x a) ∈ sβ i

Tactic:
simp [hβ.tendstoUniformlyOn_iff_of_uniformity, hl.eventually_iff]

Premises used: Filter.HasBasis.tendstoUniformlyOn_iff_of_uniformity, Filter.HasBasis.eventually_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
simp_rw : TendstoUniformlyOn F f l univ ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i
simp_rw₁ :
  (∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), Membership.mem (γ := Set α) univ x → (f x, F n x) ∈ sβ i) ↔
    ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i
simp_rw₂ :
  (∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), True → (f x, F n x) ∈ sβ i) ↔
    ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i
⊢ TendstoUniformly F f l ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i

Tactic:
simp_rw [← tendstoUniformlyOn_univ, hβ.tendstoUniformlyOn_iff_of_uniformity, mem_univ,
    true_imp_iff]

Premises used: tendstoUniformlyOn_univ, Filter.HasBasis.tendstoUniformlyOn_iff_of_uniformity, true_imp_iff, Set.mem_univ
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
X : Type u_5
ιX : Type u_6
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
pX : ιX → Prop
sX : ιX → Set X
hl : l.HasBasis pX sX
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformly F f l ↔ ∀ (i : ιβ), pβ i → ∃ (j : ιX), pX j ∧ ∀ ⦃x : X⦄, x ∈ sX j → ∀ (a : α), (f a, F x a) ∈ sβ i

Tactic:
simp only [hβ.tendstoUniformly_iff_of_uniformity, hl.eventually_iff]

Premises used: Filter.HasBasis.tendstoUniformly_iff_of_uniformity, Filter.HasBasis.eventually_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
⊢ (∀ u ∈ 𝓤 β, ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) ↔
    ∀ u ∈ 𝓤 β, ∀ᶠ (m : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.1.1 m.2, F m.1.2 m.2) ∈ u

Tactic:
forall₂_congr fun u hu => ?_

Premises used: forall₂_congr
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
refine :
  ∀ (u : Set (β × β)) (hu : u ∈ 𝓤 β),
    (∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) ↔
      ∀ᶠ (m : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.1.1 m.2, F m.1.2 m.2) ∈ u
⊢ (∀ u ∈ 𝓤 β, ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) ↔
    ∀ u ∈ 𝓤 β, ∀ᶠ (m : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.1.1 m.2, F m.1.2 m.2) ∈ u

Tactic:
refine forall₂_congr fun u hu => ?_

Premises used: forall₂_congr
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
u : Set (β × β)
hu : u ∈ 𝓤 β
rw rw₁ :
  (∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) ↔
    ∀ᶠ (x : ι × ι) in p ×ˢ p, ∀ y ∈ s, (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
⊢ (∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) ↔
    ∀ᶠ (m : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.1.1 m.2, F m.1.2 m.2) ∈ u

Tactic:
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 : ι → α → β
s : Set α
p : Filter ι
hF rwa rwa₁ rwa₂ rwa₃ : UniformCauchySeqOn F p s
⊢ UniformCauchySeqOnFilter F p (𝓟 s)

Tactic:
rwa [← uniformCauchySeqOn_iff_uniformCauchySeqOnFilter]

Premises used: uniformCauchySeqOn_iff_uniformCauchySeqOnFilter
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
rcases :
  ∀ (t : Set (β × β)) (ht : t ∈ 𝓤 β) (htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t) (htmem : SetRel.comp t t ⊆ u),
    ∀ᶠ (m : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u
⊢ ∀ᶠ (m : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u

Tactic:
rcases comp_symm_of_uniformity hu with ⟨t, ht, htsymm, htmem⟩

Premises used: comp_symm_of_uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
⊢ ∀ᶠ (x : Prod.{u_4, u_1} (ι × ι) (α × α)) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈
        t ∧
      (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈
        t

Tactic:
have := tendsto_swap4_prod.eventually ((hF t ht).prod_mk (hF t ht))
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
this :
  ∀ᶠ (x : Prod.{u_4, u_1} (ι × ι) (α × α)) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈
        t ∧
      (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈
        t
apply :
  ∀ (x : Prod.{u_4, u_1} (ι × ι) α),
    (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2,
            F (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1
              (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2) ∈
          t ∧
        (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2,
            F (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1
              (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2) ∈
          t →
      (F x.1.1 x.2, F x.1.2 x.2) ∈ u
⊢ ∀ᶠ (m : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u

Tactic:
apply this.diag_of_prod_right.mono

Premises used: Filter.Eventually.diag_of_prod_right, Filter.Eventually.mono
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
this :
  ∀ᶠ (x : Prod.{u_4, u_1} (ι × ι) (α × α)) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈
        t ∧
      (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈
        t
simp : ∀ (a b : ι) (b_1 : α), (f b_1, F a b_1) ∈ t → (f b_1, F b b_1) ∈ t → (F a b_1, F b b_1) ∈ u
⊢ ∀ (x : Prod.{u_4, u_1} (ι × ι) α),
    (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2,
            F (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1
              (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2) ∈
          t ∧
        (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2,
            F (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1
              (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2) ∈
          t →
      (F x.1.1 x.2, F x.1.2 x.2) ∈ u

Tactic:
simp only [and_imp, Prod.forall]

Premises used: and_imp, Prod.forall
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
this :
  ∀ᶠ (x : Prod.{u_4, u_1} (ι × ι) (α × α)) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈
        t ∧
      (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈
        t
n1 n2 : ι
x : α
hl : (f x, F n1 x) ∈ t
hr : (f x, F n2 x) ∈ t
⊢ (F n1 x, F n2 x) ∈ u

Tactic:
htmem <| SetRel.prodMk_mem_comp (htsymm hl) hr

Premises used: SetRel.prodMk_mem_comp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
this :
  ∀ᶠ (x : Prod.{u_4, u_1} (ι × ι) (α × α)) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈
        t ∧
      (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈
        t
n1 n2 : ι
x : α
hl : (f x, F n1 x) ∈ t
hr : (f x, F n2 x) ∈ t
⊢ (F n1 x, F n2 x) ∈ u

Tactic:
exact htmem <| SetRel.prodMk_mem_comp (htsymm hl) hr

Premises used: SetRel.prodMk_mem_comp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hF : TendstoUniformlyOn F f p s
⊢ UniformCauchySeqOn F p s

Tactic:
uniformCauchySeqOn_iff_uniformCauchySeqOnFilter.mpr
    hF.tendstoUniformlyOnFilter.uniformCauchySeqOnFilter

Premises used: Iff.mpr, uniformCauchySeqOn_iff_uniformCauchySeqOnFilter, TendstoUniformlyOnFilter.uniformCauchySeqOnFilter, 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 α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
inl :
  ∀ (hF : UniformCauchySeqOnFilter F ⊥ p') (hF' : ∀ᶠ (x : α) in p', Tendsto (fun (n : ι) ↦ F n x) ⊥ (𝓝 (f x))),
    TendstoUniformlyOnFilter F f ⊥ p'
inr : p.NeBot → TendstoUniformlyOnFilter F f p p'
⊢ TendstoUniformlyOnFilter F f p p'

Tactic:
rcases p.eq_or_neBot with rfl | _

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p' : Filter α
hF : UniformCauchySeqOnFilter F ⊥ p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun (n : ι) ↦ F n x) ⊥ (𝓝 (f x))
⊢ TendstoUniformlyOnFilter F f ⊥ p'

Tactic:
simp only [TendstoUniformlyOnFilter, bot_prod, eventually_bot, implies_true]

Premises used: TendstoUniformlyOnFilter, Filter.bot_prod, implies_true, Filter.eventually_bot
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
h : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
inr :
  ∀ (t : Set (β × β)) (ht : t ∈ 𝓤 β) (htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t) (htmem : SetRel.comp t t ⊆ u),
    ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u
⊢ ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u

Tactic:
rcases comp_symm_of_uniformity hu with ⟨t, ht, htsymm, htmem⟩

Premises used: comp_symm_of_uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
h : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
rw :
  ∃ (pa : ι × ι → Prop),
    (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
      ∃ (pb : α → Prop),
        (∀ᶠ (y : α) in p', pb y) ∧
          ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → Tendsto (fun (n : ι) ↦ F n (x, y).2) p (𝓝 (f (x, y).2))
⊢ ∀ᶠ (x : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ p', Tendsto (fun (n : ι) ↦ F n x.2) p (𝓝 (f x.2))

Tactic:
rw [eventually_prod_iff]

Premises used: Filter.eventually_prod_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
h : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
⊢ ∀ᶠ (x : ι × ι) in p ×ˢ p, (fun (x : ι × ι) ↦ True) x

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
h : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
⊢ ∀ {x : ι × ι},
    (fun (x : ι × ι) ↦ True) x →
      ∀ {y : α}, Tendsto (fun (n : ι) ↦ F n y) p (𝓝 (f y)) → Tendsto (fun (n : ι) ↦ F n (x, y).2) p (𝓝 (f (x, y).2))

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
h : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
⊢ ∃ (pa : ι × ι → Prop),
    (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
      ∃ (pb : α → Prop),
        (∀ᶠ (y : α) in p', pb y) ∧
          ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → Tendsto (fun (n : ι) ↦ F n (x, y).2) p (𝓝 (f (x, y).2))

Tactic:
exact ⟨fun _ => True, by simp, _, hF', by simp⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
h : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
⊢ ∀ᶠ (x : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ p', Tendsto (fun (n : ι) ↦ F n x.2) p (𝓝 (f x.2))

Tactic:
have hmc : ∀ᶠ x in (p ×ˢ p) ×ˢ p', Tendsto (fun n : ι => F n x.snd) p (𝓝 (f x.snd)) := by
    rw [eventually_prod_iff]
    exact ⟨fun _ => True, by simp, _, hF', by simp⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
h : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
hmc : ∀ᶠ (x : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ p', Tendsto (fun (n : ι) ↦ F n x.2) p (𝓝 (f x.2))
inr : ∀ᶠ (y : α × ι) in p' ×ˢ p, (f y.swap.2, F y.swap.1 y.swap.2) ∈ u
⊢ ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u

Tactic:
rw [Filter.eventually_swap_iff]

Premises used: Filter.eventually_swap_iff