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 : α → β
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))
⊢ ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.1
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2,
          F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.2
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) ∈
        t ∧
      Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) p
        (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2))

Tactic:
have := tendsto_prodAssoc.eventually (tendsto_prod_swap.eventually ((hF t ht).and hmc))
-- 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))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.1
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2,
          F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.2
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) ∈
        t ∧
      Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) p
        (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2))
inr :
  ∀ (x : α × ι),
    (∀ᶠ (y : ι) in p,
        (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).1.1
                (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).2,
              F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).1.2
                (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).2) ∈
            t ∧
          Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).2) p
            (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).2))) →
      (f x.swap.2, F x.swap.1 x.swap.2) ∈ u
⊢ ∀ᶠ (y : α × ι) in p' ×ˢ p, (f y.swap.2, F y.swap.1 y.swap.2) ∈ u

Tactic:
apply this.curry.mono

Premises used: Filter.Eventually.curry, 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 : 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))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.1
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2,
          F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.2
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) ∈
        t ∧
      Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) p
        (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2))
inr :
  ∀ (a : α) (b : ι),
    (∀ᶠ (x : ι) in p, (F b a, F x a) ∈ t) → Tendsto (fun (n : ι) ↦ F n a) p (𝓝 (f a)) → (f a, F b a) ∈ u
⊢ ∀ (x : α × ι),
    (∀ᶠ (y : ι) in p,
        (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).1.1
                (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).2,
              F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).1.2
                (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).2) ∈
            t ∧
          Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).2) p
            (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) (x, y))).2))) →
      (f x.swap.2, F x.swap.1 x.swap.2) ∈ u

Tactic:
simp only [Equiv.prodAssoc_apply, eventually_and, eventually_const, Prod.snd_swap, Prod.fst_swap,
    and_imp, Prod.forall]

Premises used: Filter.eventually_and, Prod.fst_swap, and_imp, Equiv.prodAssoc_apply, Filter.eventually_const, Prod.snd_swap, 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 : 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))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.1
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2,
          F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.2
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) ∈
        t ∧
      Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) p
        (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
⊢ (f x, F n x) ∈ u

Tactic:
Set.mem_of_mem_of_subset ?_ htmem

Premises used: Set.mem_of_mem_of_subset
-- 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))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.1
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2,
          F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.2
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) ∈
        t ∧
      Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) p
        (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
inr : (f x, F n x) ∈ SetRel.comp t t
⊢ (f x, F n x) ∈ u

Tactic:
refine Set.mem_of_mem_of_subset ?_ htmem

Premises used: Set.mem_of_mem_of_subset
-- 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))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.1
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2,
          F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.2
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) ∈
        t ∧
      Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) p
        (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
⊢ Tendsto (fun (x_1 : ι) ↦ (f x, F x_1 x)) p (𝓤 β)

Tactic:
rw [Uniform.tendsto_nhds_right] at hm'

Premises used: Uniform.tendsto_nhds_right
-- 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))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.1
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2,
          F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.2
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) ∈
        t ∧
      Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) p
        (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun (x_1 : ι) ↦ (f x, F x_1 x)) p (𝓤 β)
⊢ ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t ∧ (fun (x_2 : ι) ↦ (f x, F x_2 x)) x_1 ∈ t

Tactic:
have := hx.and (hm' 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 : 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))
this_1 :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.1
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2,
          F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.2
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) ∈
        t ∧
      Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) p
        (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun (x_1 : ι) ↦ (f x, F x_1 x)) p (𝓤 β)
this : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t ∧ (fun (x_2 : ι) ↦ (f x, F x_2 x)) x_1 ∈ t
inr : ∀ (m : ι) (hm : (F n x, F m x) ∈ t ∧ (fun (x_1 : ι) ↦ (f x, F x_1 x)) m ∈ t), (f x, F n x) ∈ SetRel.comp t t
⊢ (f x, F n x) ∈ SetRel.comp t t

Tactic:
obtain ⟨m, hm⟩ := this.exists

Premises used: Filter.Eventually.exists
-- 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))
this_1 :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.1
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2,
          F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.2
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) ∈
        t ∧
      Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) p
        (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun (x_1 : ι) ↦ (f x, F x_1 x)) p (𝓤 β)
this : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t ∧ (fun (x_2 : ι) ↦ (f x, F x_2 x)) x_1 ∈ t
m : ι
hm : (F n x, F m x) ∈ t ∧ (fun (x_1 : ι) ↦ (f x, F x_1 x)) m ∈ t
⊢ (f x, F n x) ∈ SetRel.comp t t

Tactic:
⟨F m x, ⟨hm.2, htsymm hm.1⟩⟩

Premises used: Set.Mem, setOf, SetRel.comp, And.right, And.left, And.intro, Exists.intro
-- 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))
this_1 :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.1
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2,
          F (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).1.2
            (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) ∈
        t ∧
      Tendsto (fun (n : ι) ↦ F n (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2) p
        (𝓝 (f (Prod.swap ((Equiv.prodAssoc α ι ι : (a : (α × ι) × ι) → α × ι × ι) x)).2))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun (x_1 : ι) ↦ (f x, F x_1 x)) p (𝓤 β)
this : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t ∧ (fun (x_2 : ι) ↦ (f x, F x_2 x)) x_1 ∈ t
m : ι
hm : (F n x, F m x) ∈ t ∧ (fun (x_1 : ι) ↦ (f x, F x_1 x)) m ∈ t
⊢ (f x, F n x) ∈ SetRel.comp t t

Tactic:
exact ⟨F m x, ⟨hm.2, htsymm hm.1⟩⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hF : UniformCauchySeqOn F p s
hF' : ∀ x ∈ s, Tendsto (fun (n : ι) ↦ F n x) p (𝓝 (f x))
⊢ TendstoUniformlyOn F f p s

Tactic:
tendstoUniformlyOn_iff_tendstoUniformlyOnFilter.mpr
    (hF.uniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto hF')

Premises used: Iff.mpr, tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto, UniformCauchySeqOn.uniformCauchySeqOnFilter
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
p'' : Filter ι
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p
⊢ UniformCauchySeqOnFilter F p'' p'

Tactic:
fun u hu =>
  (hf u hu).filter_mono (p'.prod_mono_left (Filter.prod_mono hp hp))

Premises used: Filter.Eventually.filter_mono, Filter.prod_mono, UniformCauchySeqOnFilter, Filter.prod_mono_left
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
p : Filter ι
p' p'' : Filter α
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
this : ∀ᶠ (x : Prod.{u_4, u_1} (ι × ι) α) in (p ×ˢ p) ×ˢ p'', (F x.1.1 x.2, F x.1.2 x.2) ∈ u
⊢ ∀ (x : Prod.{u_4, u_1} (ι × ι) α), (F x.1.1 x.2, F x.1.2 x.2) ∈ u → (F x.1.1 x.2, F x.1.2 x.2) ∈ u

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s s' : Set α
p : Filter ι
hf : UniformCauchySeqOn F p s
hss' : s' ⊆ s
rw : ∀ (hf : UniformCauchySeqOnFilter F p (𝓟 s)) (hss' : s' ⊆ s), UniformCauchySeqOnFilter F p (𝓟 s')
⊢ UniformCauchySeqOn F p s'

Tactic:
rw [uniformCauchySeqOn_iff_uniformCauchySeqOnFilter] at hf ⊢

Premises used: uniformCauchySeqOn_iff_uniformCauchySeqOnFilter
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s s' : Set α
p : Filter ι
hf : UniformCauchySeqOnFilter F p (𝓟 s)
hss' : s' ⊆ s
⊢ UniformCauchySeqOnFilter F p (𝓟 s')

Tactic:
hf.mono_right (le_principal_iff.mpr <| mem_principal.mpr hss')

Premises used: Iff.mpr, Filter.le_principal_iff, Filter.mem_principal, UniformCauchySeqOnFilter.mono_right
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
s s' : Set α
p : Filter ι
hf : UniformCauchySeqOnFilter F p (𝓟 s)
hss' : s' ⊆ s
⊢ UniformCauchySeqOnFilter F p (𝓟 s')

Tactic:
exact hf.mono_right (le_principal_iff.mpr <| mem_principal.mpr hss')

Premises used: Iff.mpr, Filter.le_principal_iff, Filter.mem_principal, UniformCauchySeqOnFilter.mono_right
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
γ : Type u_5
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
obtain :
  ∀ (pa : ι × ι → Prop) (hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) (pb : α → Prop) (hpb : ∀ᶠ (y : α) in p', pb y)
    (hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u),
    ∀ᶠ (m : Prod.{u_4, u_5} (ι × ι) γ) in (p ×ˢ p) ×ˢ comap g p',
      ((fun (n : ι) ↦ F n ∘ g) m.1.1 m.2, (fun (n : ι) ↦ F n ∘ g) m.1.2 m.2) ∈ u
⊢ ∀ᶠ (m : Prod.{u_4, u_5} (ι × ι) γ) in (p ×ˢ p) ×ˢ comap g p',
    ((fun (n : ι) ↦ F n ∘ g) m.1.1 m.2, (fun (n : ι) ↦ F n ∘ g) m.1.2 m.2) ∈ u

Tactic:
obtain ⟨pa, hpa, pb, hpb, hpapb⟩ := eventually_prod_iff.mp (hf u hu)

Premises used: Filter.eventually_prod_iff, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
γ : Type u_5
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
rw :
  ∃ (pa : ι × ι → Prop),
    (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
      ∃ (pb : γ → Prop),
        (∀ᶠ (y : γ) in comap g p', pb y) ∧
          ∀ {x : ι × ι},
            pa x →
              ∀ {y : γ},
                pb y → ((fun (n : ι) ↦ F n ∘ g) (x, y).1.1 (x, y).2, (fun (n : ι) ↦ F n ∘ g) (x, y).1.2 (x, y).2) ∈ u
⊢ ∀ᶠ (m : Prod.{u_4, u_5} (ι × ι) γ) in (p ×ˢ p) ×ˢ comap g p',
    ((fun (n : ι) ↦ F n ∘ g) m.1.1 m.2, (fun (n : ι) ↦ F n ∘ g) m.1.2 m.2) ∈ u

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 : ι → α → β
p : Filter ι
p' : Filter α
γ : Type u_5
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
⊢ ∃ (pa : ι × ι → Prop),
    (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
      ∃ (pb : γ → Prop),
        (∀ᶠ (y : γ) in comap g p', pb y) ∧
          ∀ {x : ι × ι},
            pa x →
              ∀ {y : γ},
                pb y → ((fun (n : ι) ↦ F n ∘ g) (x, y).1.1 (x, y).2, (fun (n : ι) ↦ F n ∘ g) (x, y).1.2 (x, y).2) ∈ u

Tactic:
⟨pa, hpa, pb ∘ g, ?_, fun hx _ hy => hpapb hx hy⟩

Premises used: Function.comp, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
γ : Type u_5
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
refine : ∀ᶠ (y : γ) in comap g p', (pb ∘ g) y
⊢ ∃ (pa : ι × ι → Prop),
    (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
      ∃ (pb : γ → Prop),
        (∀ᶠ (y : γ) in comap g p', pb y) ∧
          ∀ {x : ι × ι},
            pa x →
              ∀ {y : γ},
                pb y → ((fun (n : ι) ↦ F n ∘ g) (x, y).1.1 (x, y).2, (fun (n : ι) ↦ F n ∘ g) (x, y).1.2 (x, y).2) ∈ u

Tactic:
refine ⟨pa, hpa, pb ∘ g, ?_, fun hx _ hy => hpapb hx hy⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
γ : Type u_5
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
x : α
hx : pb x
y : γ
hy : g y = x
⊢ (pb ∘ g) y

Tactic:
simp only [hx, hy, Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.Topology.UniformSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
F : ι → α → β
p : Filter ι
p' : Filter α
γ : Type u_5
hf : UniformCauchySeqOnFilter F p p'
g : γ → α
u : Set (β × β)
hu : u ∈ 𝓤 β
pa : ι × ι → Prop
hpa : ∀ᶠ (x : ι × ι) in p ×ˢ p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in p', pb y
hpapb : ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u
⊢ ∀ᶠ (y : γ) in comap g p', (pb ∘ g) y

Tactic:
exact eventually_comap.mpr (hpb.mono fun x hx y hy => by simp only [hx, hy, Function.comp_apply])

Premises used: Iff.mpr, Filter.Eventually.mono, Filter.eventually_comap
-- 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 : UniformCauchySeqOn F p s
g : γ → α
rw :
  ∀ (hf : UniformCauchySeqOnFilter F p (𝓟 s)) (g : γ → α),
    UniformCauchySeqOnFilter.{u_5, u_2, u_4} (β := β) (fun (n : ι) ↦ F n ∘ g) p (𝓟 (g ⁻¹' s))
⊢ UniformCauchySeqOn.{u_5, u_2, u_4} (β := β) (fun (n : ι) ↦ F n ∘ g) p (g ⁻¹' s)

Tactic:
rw [uniformCauchySeqOn_iff_uniformCauchySeqOnFilter] at hf ⊢

Premises used: uniformCauchySeqOn_iff_uniformCauchySeqOnFilter