-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem EquicontinuousAt.tendsto_of_mem_closure {l : Filter ι} {F : ι → X → α} {f : X → α}
    {s : Set X} {x : X} {z : α} (hF : EquicontinuousAt F x) (hf : Tendsto f (𝓝[s] x) (𝓝 z))
    (hs : ∀ y ∈ s, Tendsto (F · y) l (𝓝 (f y))) (hx : x ∈ closure s) :
    Tendsto (F · x) l (𝓝 z)

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))
hx : x ∈ closure s
⊢ ∀ i ∈ 𝓤 α, ∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id i}

Tactic:
intro U hU

Result:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))
hx : x ∈ closure s
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}

Proof state:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))
hx : (𝓝[s] x).NeBot
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
this : ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V
y : X
hys : y ∈ s
hFy : ∀ (i : ι), (F i x, F i y) ∈ V
hfy : (f y, z) ∈ V
⊢ ∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}

Tactic:
filter_upwards [hs y hys (ball_mem_nhds _ hV)] with i hi

Result:
case h
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))
hx : (𝓝[s] x).NeBot
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
this : ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V
y : X
hys : y ∈ s
hFy : ∀ (i : ι), (F i x, F i y) ∈ V
hfy : (f y, z) ∈ V
i : ι
hi : i ∈ (fun x => F x y) ⁻¹' ball (f y) V
⊢ (F i x, z) ∈ id U

Proof state:
case intro.intro.intro
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))
hx : (𝓝[s] x).NeBot
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
this : ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V
⊢ ∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}

Tactic:
rcases this.exists with ⟨y, hys, hFy, hfy⟩

Result:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))
hx : (𝓝[s] x).NeBot
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
this : ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V
y : X
hys : y ∈ s
hFy : ∀ (i : ι), (F i x, F i y) ∈ V
hfy : (f y, z) ∈ V
⊢ ∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}

Proof state:
case h
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))
hx : (𝓝[s] x).NeBot
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
this : ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V
y : X
hys : y ∈ s
hFy : ∀ (i : ι), (F i x, F i y) ∈ V
hfy : (f y, z) ∈ V
i : ι
hi : i ∈ (fun x => F x y) ⁻¹' ball (f y) V
⊢ (F i x, z) ∈ id U

Tactic:
exact hVU ⟨_, ⟨_, hFy i, (mem_ball_symmetry hVs).2 hi⟩, hfy⟩

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : Tendsto f (𝓝[s] x) (𝓝 z)
hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))
hx : x ∈ closure s
⊢ Tendsto (fun x_1 => F x_1 x) l (𝓝 z)

Tactic:
rw [(nhds_basis_uniformity (𝓤 α).basis_sets).tendsto_right_iff] at hf ⊢

Result:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))
hx : x ∈ closure s
⊢ ∀ i ∈ 𝓤 α, ∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id i}

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))
hx : x ∈ closure s
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}

Tactic:
rcases comp_comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVs, hVU⟩

Result:
case intro.intro.intro
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))
hx : x ∈ closure s
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
⊢ ∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}

Proof state:
case intro.intro.intro
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))
hx : x ∈ closure s
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
⊢ ∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}

Tactic:
rw [mem_closure_iff_nhdsWithin_neBot] at hx

Result:
case intro.intro.intro
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))
hx : (𝓝[s] x).NeBot
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
⊢ ∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}