-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem Filter.Tendsto.continuousWithinAt_of_equicontinuousWithinAt {l : Filter ι} [l.NeBot]
    {F : ι → X → α} {f : X → α} {S : Set X} {x₀ : X} (h₁ : ∀ x ∈ S, Tendsto (F · x) l (𝓝 (f x)))
    (h₂ : Tendsto (F · x₀) l (𝓝 (f x₀))) (h₃ : EquicontinuousWithinAt F S x₀) :
    ContinuousWithinAt f S x₀

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
S : Set X
x₀ : X
h₁ : ∀ x ∈ S, Tendsto (fun x_1 => F x_1 x) l (𝓝 (f x))
h₂ : Tendsto (fun x => F x x₀) l (𝓝 (f x₀))
h₃ : EquicontinuousWithinAt F S x₀
⊢ ContinuousWithinAt f S x₀

Tactic:
intro U hU

Result:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
S : Set X
x₀ : X
h₁ : ∀ x ∈ S, Tendsto (fun x_1 => F x_1 x) l (𝓝 (f x))
h₂ : Tendsto (fun x => F x x₀) l (𝓝 (f x₀))
h₃ : EquicontinuousWithinAt F S x₀
U : Set α
hU : U ∈ 𝓝 (f x₀)
⊢ U ∈ map f (𝓝[S] x₀)

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
S : Set X
x₀ : X
h₁ : ∀ x ∈ S, Tendsto (fun x_1 => F x_1 x) l (𝓝 (f x))
h₂ : Tendsto (fun x => F x x₀) l (𝓝 (f x₀))
h₃ : EquicontinuousWithinAt F S x₀
U : Set α
hU : U ∈ 𝓝 (f x₀)
⊢ U ∈ map f (𝓝[S] x₀)

Tactic:
rw [mem_map]

Result:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
S : Set X
x₀ : X
h₁ : ∀ x ∈ S, Tendsto (fun x_1 => F x_1 x) l (𝓝 (f x))
h₂ : Tendsto (fun x => F x x₀) l (𝓝 (f x₀))
h₃ : EquicontinuousWithinAt F S x₀
U : Set α
hU : U ∈ 𝓝 (f x₀)
⊢ f ⁻¹' U ∈ 𝓝[S] x₀

Proof state:
case intro.intro.intro.intro.intro
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
S : Set X
x₀ : X
h₁ : ∀ x ∈ S, Tendsto (fun x_1 => F x_1 x) l (𝓝 (f x))
h₂ : Tendsto (fun x => F x x₀) l (𝓝 (f x₀))
h₃ : EquicontinuousWithinAt F S x₀
U : Set α
hU : U ∈ 𝓝 (f x₀)
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : ball (f x₀) V ⊆ U
W : Set (α × α)
hW : W ∈ 𝓤 α
hWclosed : IsClosed W
hWV : W ⊆ V
⊢ f ⁻¹' U ∈ 𝓝[S] x₀

Tactic:
filter_upwards [h₃ W hW, eventually_mem_nhdsWithin] with x hx hxS using
  hVU <| ball_mono hWV (f x₀) <| hWclosed.mem_of_tendsto (h₂.prod_mk_nhds (h₁ x hxS)) <|
  Eventually.of_forall hx

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
S : Set X
x₀ : X
h₁ : ∀ x ∈ S, Tendsto (fun x_1 => F x_1 x) l (𝓝 (f x))
h₂ : Tendsto (fun x => F x x₀) l (𝓝 (f x₀))
h₃ : EquicontinuousWithinAt F S x₀
U : Set α
hU : U ∈ 𝓝 (f x₀)
⊢ f ⁻¹' U ∈ 𝓝[S] x₀

Tactic:
rcases UniformSpace.mem_nhds_iff.mp hU with ⟨V, hV, hVU⟩

Result:
case intro.intro
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
S : Set X
x₀ : X
h₁ : ∀ x ∈ S, Tendsto (fun x_1 => F x_1 x) l (𝓝 (f x))
h₂ : Tendsto (fun x => F x x₀) l (𝓝 (f x₀))
h₃ : EquicontinuousWithinAt F S x₀
U : Set α
hU : U ∈ 𝓝 (f x₀)
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : ball (f x₀) V ⊆ U
⊢ f ⁻¹' U ∈ 𝓝[S] x₀

Proof state:
case intro.intro
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
S : Set X
x₀ : X
h₁ : ∀ x ∈ S, Tendsto (fun x_1 => F x_1 x) l (𝓝 (f x))
h₂ : Tendsto (fun x => F x x₀) l (𝓝 (f x₀))
h₃ : EquicontinuousWithinAt F S x₀
U : Set α
hU : U ∈ 𝓝 (f x₀)
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : ball (f x₀) V ⊆ U
⊢ f ⁻¹' U ∈ 𝓝[S] x₀

Tactic:
rcases mem_uniformity_isClosed hV with ⟨W, hW, hWclosed, hWV⟩

Result:
case intro.intro.intro.intro.intro
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
S : Set X
x₀ : X
h₁ : ∀ x ∈ S, Tendsto (fun x_1 => F x_1 x) l (𝓝 (f x))
h₂ : Tendsto (fun x => F x x₀) l (𝓝 (f x₀))
h₃ : EquicontinuousWithinAt F S x₀
U : Set α
hU : U ∈ 𝓝 (f x₀)
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : ball (f x₀) V ⊆ U
W : Set (α × α)
hW : W ∈ 𝓤 α
hWclosed : IsClosed W
hWV : W ⊆ V
⊢ f ⁻¹' U ∈ 𝓝[S] x₀