-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto
    (hF : UniformCauchySeqOnFilter F p p')
    (hF' : ∀ᶠ x : α in p', Tendsto (fun n => F n x) p (𝓝 (f x))) :
    TendstoUniformlyOnFilter F f p p'

Proof state:
case inr.intro.intro.intro
α : Type u
β : Type v
ι : Type x
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 : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))
this✝ :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2,
          F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈
        t ∧
      Tendsto (fun n => F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.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
⊢ ∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t

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

Result:
case inr.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
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 : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))
this✝ :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2,
          F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈
        t ∧
      Tendsto (fun n => F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.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
⊢ ∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t

Proof state:
case inr.intro.intro.intro
α : Type u
β : Type v
ι : Type x
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 : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2,
          F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈
        t ∧
      Tendsto (fun n => F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.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:
refine Set.mem_of_mem_of_subset (mem_compRel.mpr ?_) htmem

Result:
case inr.intro.intro.intro
α : Type u
β : Type v
ι : Type x
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 : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2,
          F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈
        t ∧
      Tendsto (fun n => F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.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))
⊢ ∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t

Proof state:
case inr.intro.intro.intro
α : Type u
β : Type v
ι : Type x
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 : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2,
          F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈
        t ∧
      Tendsto (fun n => F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.2))
⊢ ∀ᶠ (y : α × ι) in p' ×ˢ p, (f y.swap.2, F y.swap.1 y.swap.2) ∈ u

Tactic:
apply this.curry.mono

Result:
case inr.intro.intro.intro
α : Type u
β : Type v
ι : Type x
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 : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2,
          F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈
        t ∧
      Tendsto (fun n => F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.2))
⊢ ∀ (x : α × ι),
    (∀ᶠ (y : ι) in p,
        (F ((Equiv.prodAssoc α ι ι) (x, y)).swap.1.1 ((Equiv.prodAssoc α ι ι) (x, y)).swap.2,
              F ((Equiv.prodAssoc α ι ι) (x, y)).swap.1.2 ((Equiv.prodAssoc α ι ι) (x, y)).swap.2) ∈
            t ∧
          Tendsto (fun n => F n ((Equiv.prodAssoc α ι ι) (x, y)).swap.2) p
            (𝓝 (f ((Equiv.prodAssoc α ι ι) (x, y)).swap.2))) →
      (f x.swap.2, F x.swap.1 x.swap.2) ∈ u

Proof state:
case inr.intro.intro.intro
α : Type u
β : Type v
ι : Type x
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 : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))
⊢ ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u

Tactic:
rw [Filter.eventually_swap_iff]

Result:
case inr.intro.intro.intro
α : Type u
β : Type v
ι : Type x
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 : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))
⊢ ∀ᶠ (y : α × ι) in p' ×ˢ p, (f y.swap.2, F y.swap.1 y.swap.2) ∈ u