-- 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:
α : 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
⊢ ∃ pa,
    (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
      ∃ pb,
        (∀ᶠ (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⟩

Result:
no goals

Proof state:
case inl
α : Type u
β : Type v
ι : Type x
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]

Result:
no goals

Proof state:
α : 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
⊢ ∀ {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

Result:
no goals

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
⊢ ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u

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⟩

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))
⊢ ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.2, F n.1 n.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))
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

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

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))
⊢ ∀ (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

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))
⊢ ∀ (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

Tactic:
intro x n hx hm'

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))
⊢ (f x, F n x) ∈ u