-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem EquicontinuousWithinAt.closure' {A : Set Y} {u : Y → X → α} {S : Set X} {x₀ : X}
    (hA : EquicontinuousWithinAt (u ∘ (↑) : A → X → α) S x₀) (hu₁ : Continuous (S.restrict ∘ u))
    (hu₂ : Continuous (eval x₀ ∘ u)) :
    EquicontinuousWithinAt (u ∘ (↑) : closure A → X → α) S x₀

Proof state:
case h
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous (S.restrict ∘ u)
hu₂ : Continuous (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x : X
hxS : x ∈ S
hx : A ⊆ (fun f => (u f x₀, u f x)) ⁻¹' V
⊢ ∀ (x_1 : Y) (h : x_1 ∈ closure A), ((u ∘ Subtype.val) ⟨x_1, h⟩ x₀, (u ∘ Subtype.val) ⟨x_1, h⟩ x) ∈ U

Tactic:
refine (closure_minimal hx <| hVclosed.preimage <| hu₂.prod_mk ?_).trans (preimage_mono hVU)

Result:
case h
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous (S.restrict ∘ u)
hu₂ : Continuous (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x : X
hxS : x ∈ S
hx : A ⊆ (fun f => (u f x₀, u f x)) ⁻¹' V
⊢ Continuous fun f => u f x

Proof state:
case h
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous (S.restrict ∘ u)
hu₂ : Continuous (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x : X
hxS : x ∈ S
hx : A ⊆ (fun f => (u f x₀, u f x)) ⁻¹' V
⊢ Continuous fun f => u f x

Tactic:
exact (continuous_apply ⟨x, hxS⟩).comp hu₁

Result:
no goals

Proof state:
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous (S.restrict ∘ u)
hu₂ : Continuous (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U

Tactic:
rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩

Result:
case intro.intro.intro
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous (S.restrict ∘ u)
hu₂ : Continuous (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U

Proof state:
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous (S.restrict ∘ u)
hu₂ : Continuous (eval x₀ ∘ u)
⊢ EquicontinuousWithinAt (u ∘ Subtype.val) S x₀

Tactic:
intro U hU

Result:
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous (S.restrict ∘ u)
hu₂ : Continuous (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U

Proof state:
case h
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous (S.restrict ∘ u)
hu₂ : Continuous (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x : X
hx : ∀ (x_1 : Y) (h : x_1 ∈ A), ((u ∘ Subtype.val) ⟨x_1, h⟩ x₀, (u ∘ Subtype.val) ⟨x_1, h⟩ x) ∈ V
hxS : x ∈ S
⊢ ∀ (x_1 : Y) (h : x_1 ∈ closure A), ((u ∘ Subtype.val) ⟨x_1, h⟩ x₀, (u ∘ Subtype.val) ⟨x_1, h⟩ x) ∈ U

Tactic:
change A ⊆ (fun f => (u f x₀, u f x)) ⁻¹' V at hx

Result:
case h
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous (S.restrict ∘ u)
hu₂ : Continuous (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x : X
hxS : x ∈ S
hx : A ⊆ (fun f => (u f x₀, u f x)) ⁻¹' V
⊢ ∀ (x_1 : Y) (h : x_1 ∈ closure A), ((u ∘ Subtype.val) ⟨x_1, h⟩ x₀, (u ∘ Subtype.val) ⟨x_1, h⟩ x) ∈ U

Proof state:
case intro.intro.intro
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous (S.restrict ∘ u)
hu₂ : Continuous (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U

Tactic:
filter_upwards [hA V hV, eventually_mem_nhdsWithin] with x hx hxS

Result:
case h
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous (S.restrict ∘ u)
hu₂ : Continuous (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x : X
hx : ∀ (i : ↑A), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ V
hxS : x ∈ S
⊢ ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U

Proof state:
case h
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous (S.restrict ∘ u)
hu₂ : Continuous (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x : X
hx : ∀ (i : ↑A), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ V
hxS : x ∈ S
⊢ ∀ (i : ↑(closure A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U

Tactic:
rw [SetCoe.forall] at *

Result:
case h
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous (S.restrict ∘ u)
hu₂ : Continuous (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed V
hVU : V ⊆ U
x : X
hx : ∀ (x_1 : Y) (h : x_1 ∈ A), ((u ∘ Subtype.val) ⟨x_1, h⟩ x₀, (u ∘ Subtype.val) ⟨x_1, h⟩ x) ∈ V
hxS : x ∈ S
⊢ ∀ (x_1 : Y) (h : x_1 ∈ closure A), ((u ∘ Subtype.val) ⟨x_1, h⟩ x₀, (u ∘ Subtype.val) ⟨x_1, h⟩ x) ∈ U