-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoLocallyUniformlyOn_iff_filter :
    TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, TendstoUniformlyOnFilter F f p (𝓝[s] x)

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
⊢ TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, TendstoUniformlyOnFilter F f p (𝓝[s] x)

Tactic:
simp only [TendstoUniformlyOnFilter, eventually_prod_iff]

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
⊢ TendstoLocallyUniformlyOn F f p s ↔
    ∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ pa,
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u

Proof state:
case mpr
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
⊢ (∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ pa,
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u) →
    TendstoLocallyUniformlyOn F f p s

Tactic:
rintro h u hu x hx

Result:
case mpr
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
h :
  ∀ x ∈ s,
    ∀ u ∈ 𝓤 β,
      ∃ pa,
        (∀ᶠ (x : ι) in p, pa x) ∧
          ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Proof state:
case mp
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
⊢ TendstoLocallyUniformlyOn F f p s →
    ∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ pa,
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u

Tactic:
rintro h x hx u hu

Result:
case mp
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∃ pa,
    (∀ᶠ (x : ι) in p, pa x) ∧ ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u

Proof state:
case mpr.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
h✝ :
  ∀ x ∈ s,
    ∀ u ∈ 𝓤 β,
      ∃ pa,
        (∀ᶠ (x : ι) in p, pa x) ∧
          ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
pa : ι → Prop
hpa : ∀ᶠ (x : ι) in p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in 𝓝[s] x, pb y
h : ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
exact ⟨pb, hpb, eventually_of_mem hpa fun i hi y hy => h hi hy⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
⊢ TendstoLocallyUniformlyOn F f p s ↔
    ∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ pa,
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u

Tactic:
constructor

Result:
case mp
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
⊢ TendstoLocallyUniformlyOn F f p s →
    ∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ pa,
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u

case mpr
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
⊢ (∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ pa,
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u) →
    TendstoLocallyUniformlyOn F f p s

Proof state:
case mpr
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
h :
  ∀ x ∈ s,
    ∀ u ∈ 𝓤 β,
      ∃ pa,
        (∀ᶠ (x : ι) in p, pa x) ∧
          ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
obtain ⟨pa, hpa, pb, hpb, h⟩ := h x hx u hu

Result:
case mpr.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
h✝ :
  ∀ x ∈ s,
    ∀ u ∈ 𝓤 β,
      ∃ pa,
        (∀ᶠ (x : ι) in p, pa x) ∧
          ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
pa : ι → Prop
hpa : ∀ᶠ (x : ι) in p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in 𝓝[s] x, pb y
h : ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Proof state:
case mp.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s✝ : Set α
p : Filter ι
inst✝ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s✝
x : α
hx : x ∈ s✝
u : Set (β × β)
hu : u ∈ 𝓤 β
s : Set α
hs1 : s ∈ 𝓝[s✝] x
hs2 : ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, F n y) ∈ u
⊢ ∃ pa,
    (∀ᶠ (x : ι) in p, pa x) ∧ ∃ pb, (∀ᶠ (y : α) in 𝓝[s✝] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u

Tactic:
exact ⟨_, hs2, _, eventually_of_mem hs1 fun x => id, fun hi y hy => hi y hy⟩

Result:
no goals

Proof state:
case mp
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∃ pa,
    (∀ᶠ (x : ι) in p, pa x) ∧ ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u

Tactic:
obtain ⟨s, hs1, hs2⟩ := h u hu x hx

Result:
case mp.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s✝ : Set α
p : Filter ι
inst✝ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s✝
x : α
hx : x ∈ s✝
u : Set (β × β)
hu : u ∈ 𝓤 β
s : Set α
hs1 : s ∈ 𝓝[s✝] x
hs2 : ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, F n y) ∈ u
⊢ ∃ pa,
    (∀ᶠ (x : ι) in p, pa x) ∧ ∃ pb, (∀ᶠ (y : α) in 𝓝[s✝] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u