-- Mathlib/Topology/EMetricSpace/Basic.lean
theorem tendstoLocallyUniformlyOn_iff {ι : Type*} [TopologicalSpace β] {F : ι → β → α} {f : β → α}
    {p : Filter ι} {s : Set β} :
    TendstoLocallyUniformlyOn F f p s ↔
      ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ n in p, ∀ y ∈ t, edist (f y) (F n y) < ε

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
ι : Type u_2
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
rcases mem_uniformity_edist.1 hu with ⟨ε, εpos, hε⟩

Result:
case intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
ι : Type u_2
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ≥0∞
εpos : ε > 0
hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Proof state:
case intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
ι : Type u_2
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ≥0∞
εpos : ε > 0
hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
rcases H ε εpos x hx with ⟨t, ht, Ht⟩

Result:
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
ι : Type u_2
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ≥0∞
εpos : ε > 0
hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u
t : Set β
ht : t ∈ 𝓝[s] x
Ht : ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Proof state:
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
ι : Type u_2
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ≥0∞
εpos : ε > 0
hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u
t : Set β
ht : t ∈ 𝓝[s] x
Ht : ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
exact ⟨t, ht, Ht.mono fun n hs x hx => hε (hs x hx)⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
ι : Type u_2
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
⊢ TendstoLocallyUniformlyOn F f p s ↔ ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε

Tactic:
refine ⟨fun H ε hε => H _ (edist_mem_uniformity hε), fun H u hu x hx => ?_⟩

Result:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
ι : Type u_2
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u