awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
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 (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : X) ↦ α) ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval (β := fun (x : X) ↦ α) x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x : X
hx :
  ∀ (i : (↑A : Type u_5)),
    ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) i x₀, (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) i x) ∈ V
hxS : x ∈ S
h :
  ∀
    (hx :
      ∀ (x_1 : Y) (h : x_1 ∈ A),
        ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) (Subtype.mk (p := fun (x : Y) ↦ x ∈ A) x_1 h) x₀,
            (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) (Subtype.mk (p := fun (x : Y) ↦ x ∈ A) x_1 h) x) ∈
          V)
    (hxS : x ∈ S) (x_1 : Y) (h : x_1 ∈ closure[tY] A),
    ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) (Subtype.mk (p := fun (x : Y) ↦ x ∈ closure[tY] A) x_1 h)
          x₀,
        (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A))
          (Subtype.mk (p := fun (x : Y) ↦ x ∈ closure[tY] A) x_1 h) x) ∈
      U
⊢ ∀ (i : (↑(closure[tY] A) : Type u_5)),
    ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i x₀,
        (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i x) ∈
      U

Tactic:
rw [SetCoe.forall] at *

Premises used: SetCoe.forall
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
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 (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : X) ↦ α) ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval (β := fun (x : X) ↦ α) x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x : X
hx :
  ∀ (x_1 : Y) (h : x_1 ∈ A),
    ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) (Subtype.mk (p := fun (x : Y) ↦ x ∈ A) x_1 h) x₀,
        (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) (Subtype.mk (p := fun (x : Y) ↦ x ∈ A) x_1 h) x) ∈
      V
hxS : x ∈ S
⊢ A ⊆ (fun (f : Y) ↦ (u f x₀, u f x)) ⁻¹' V

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

Premises used: Prod.mk
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
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 (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : X) ↦ α) ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval (β := fun (x : X) ↦ α) x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x : X
hxS : x ∈ S
hx : A ⊆ (fun (f : Y) ↦ (u f x₀, u f x)) ⁻¹' V
⊢ ∀ (x_1 : Y) (h : x_1 ∈ closure[tY] A),
    ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) (Subtype.mk (p := fun (x : Y) ↦ x ∈ closure[tY] A) x_1 h)
          x₀,
        (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A))
          (Subtype.mk (p := fun (x : Y) ↦ x ∈ closure[tY] A) x_1 h) x) ∈
      U

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

Premises used: Set.Mem, closure_minimal, setOf, HasSubset.Subset.trans, Set.Subset, Set.preimage_mono, Set.preimage, IsClosed.preimage, Continuous.prodMk
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
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 (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : X) ↦ α) ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval (β := fun (x : X) ↦ α) x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x : X
hxS : x ∈ S
hx : A ⊆ (fun (f : Y) ↦ (u f x₀, u f x)) ⁻¹' V
h : Continuous[tY, uα.toTopologicalSpace] fun (f : Y) ↦ u f x
⊢ ∀ (x_1 : Y) (h : x_1 ∈ closure[tY] A),
    ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) (Subtype.mk (p := fun (x : Y) ↦ x ∈ closure[tY] A) x_1 h)
          x₀,
        (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A))
          (Subtype.mk (p := fun (x : Y) ↦ x ∈ closure[tY] A) x_1 h) x) ∈
      U

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

Premises used: closure_minimal, HasSubset.Subset.trans, Set.preimage_mono, IsClosed.preimage, Continuous.prodMk
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
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 (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : X) ↦ α) ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval (β := fun (x : X) ↦ α) x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x : X
hxS : x ∈ S
hx : A ⊆ (fun (f : Y) ↦ (u f x₀, u f x)) ⁻¹' V
⊢ Continuous[tY, uα.toTopologicalSpace] fun (f : Y) ↦ u f x

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

Premises used: Continuous.comp, continuous_apply, Set.restrict
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
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 (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : X) ↦ α) ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval (β := fun (x : X) ↦ α) x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x : X
hxS : x ∈ S
hx : A ⊆ (fun (f : Y) ↦ (u f x₀, u f x)) ⁻¹' V
⊢ Continuous[tY, uα.toTopologicalSpace] fun (f : Y) ↦ u f x

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

Premises used: Continuous.comp, continuous_apply
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
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 → α
x₀ : X
hA : EquicontinuousAt (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) x₀
hu : Continuous[tY, Pi.topologicalSpace] u
rw :
  ∀ (hA : EquicontinuousWithinAt (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) univ x₀)
    (hu : Continuous[tY, Pi.topologicalSpace] u),
    EquicontinuousWithinAt (ι := (↑(closure[tY] A) : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A))
      univ x₀
⊢ EquicontinuousAt (ι := (↑(closure[tY] A) : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) x₀

Tactic:
rw [← equicontinuousWithinAt_univ] at hA ⊢

Premises used: equicontinuousWithinAt_univ
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
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 → α
x₀ : X
hA : EquicontinuousWithinAt (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) univ x₀
hu : Continuous[tY, Pi.topologicalSpace] u
⊢ EquicontinuousWithinAt (ι := (↑(closure[tY] A) : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A))
    univ x₀

Tactic:
hA.closure' (Pi.continuous_restrict _ |>.comp hu) (continuous_apply x₀ |>.comp hu)

Premises used: Continuous.comp, Pi.continuous_restrict, continuous_apply, EquicontinuousWithinAt.closure'
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
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 → α
x₀ : X
hA : EquicontinuousWithinAt (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) univ x₀
hu : Continuous[tY, Pi.topologicalSpace] u
⊢ EquicontinuousWithinAt (ι := (↑(closure[tY] A) : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A))
    univ x₀

Tactic:
exact hA.closure' (Pi.continuous_restrict _ |>.comp hu) (continuous_apply x₀ |>.comp hu)

Premises used: Continuous.comp, Pi.continuous_restrict, continuous_apply, EquicontinuousWithinAt.closure'
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
A : Set (X → α)
x₀ : X
hA : A.EquicontinuousAt x₀
⊢ (closure[Pi.topologicalSpace] A).EquicontinuousAt x₀

Tactic:
hA.closure' (u := id) continuous_id

Premises used: EquicontinuousAt.closure', Set.Mem, continuous_id
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
A : Set (X → α)
S : Set X
x₀ : X
hA : A.EquicontinuousWithinAt S x₀
⊢ (closure[Pi.topologicalSpace] A).EquicontinuousWithinAt S x₀

Tactic:
hA.closure' (u := id) (Pi.continuous_restrict _) (continuous_apply _)

Premises used: Set.Mem, Pi.continuous_restrict, continuous_apply, EquicontinuousWithinAt.closure'
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
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 → α
hA : Equicontinuous (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A))
hu : Continuous[tY, Pi.topologicalSpace] u
⊢ Equicontinuous (ι := (↑(closure[tY] A) : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A))

Tactic:
fun x ↦ (hA x).closure' hu

Premises used: EquicontinuousAt.closure', Equicontinuous
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
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
hA : EquicontinuousOn (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S
hu : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : X) ↦ α) ∘ u)
x : X
hx : x ∈ S
⊢ Continuous[tY, uα.toTopologicalSpace] (eval (β := fun (x : X) ↦ α) x ∘ u)

Tactic:
continuous_apply ⟨x, hx⟩ |>.comp hu

Premises used: Continuous.comp, continuous_apply, Set.restrict
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
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
hA : EquicontinuousOn (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S
hu : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : X) ↦ α) ∘ u)
x : X
hx : x ∈ S
⊢ Continuous[tY, uα.toTopologicalSpace] (eval (β := fun (x : X) ↦ α) x ∘ u)

Tactic:
exact continuous_apply ⟨x, hx⟩ |>.comp hu

Premises used: Continuous.comp, continuous_apply
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
A : Set (X → α)
hA : A.Equicontinuous
⊢ (closure[Pi.topologicalSpace] A).Equicontinuous

Tactic:
fun x ↦ Set.EquicontinuousAt.closure (hA x)

Premises used: Equicontinuous, Set.EquicontinuousAt.closure
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
A : Set (X → α)
S : Set X
hA : A.EquicontinuousOn S
⊢ (closure[Pi.topologicalSpace] A).EquicontinuousOn S

Tactic:
fun x hx ↦ Set.EquicontinuousWithinAt.closure (hA x hx)

Premises used: EquicontinuousOn, Set.EquicontinuousWithinAt.closure
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S
hu : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : β) ↦ α) ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
rcases :
  ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVclosed : IsClosed[instTopologicalSpaceProd] V) (hVU : V ⊆ U),
    ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S),
      ∀ (i : (↑(closure[tY] A) : Type u_5)),
        ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i xy.1,
            (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i xy.2) ∈
          U
⊢ ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S),
    ∀ (i : (↑(closure[tY] A) : Type u_5)),
      ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i xy.1,
          (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i xy.2) ∈
        U

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

Premises used: mem_uniformity_isClosed
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S
hu : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : β) ↦ α) ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
h :
  ∀ (a : β × β),
    (∀ (i : (↑A : Type u_5)),
        ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) i a.1, (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) i a.2) ∈ V) →
      a ∈ S ×ˢ S →
        ∀ (i : (↑(closure[tY] A) : Type u_5)),
          ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i a.1,
              (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i a.2) ∈
            U
⊢ ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S),
    ∀ (i : (↑(closure[tY] A) : Type u_5)),
      ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i xy.1,
          (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i xy.2) ∈
        U

Tactic:
filter_upwards [hA V hV, mem_inf_of_right (mem_principal_self _)]

Premises used: Filter.mem_principal_self, Filter.mem_inf_of_right
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S
hu : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : β) ↦ α) ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x y : β
hxy :
  ∀ (i : (↑A : Type u_5)),
    ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) i (x, y).1, (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) i (x, y).2) ∈
      V
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
h :
  ∀
    (hxy :
      ∀ (x_1 : Y) (h : x_1 ∈ A),
        ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) (Subtype.mk (p := fun (x : Y) ↦ x ∈ A) x_1 h) (x, y).1,
            (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) (Subtype.mk (p := fun (x : Y) ↦ x ∈ A) x_1 h) (x, y).2) ∈
          V)
    (hxS : (x, y).1 ∈ S) (hyS : (x, y).2 ∈ S) (x_1 : Y) (h : x_1 ∈ closure[tY] A),
    ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) (Subtype.mk (p := fun (x : Y) ↦ x ∈ closure[tY] A) x_1 h)
          (x, y).1,
        (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A))
          (Subtype.mk (p := fun (x : Y) ↦ x ∈ closure[tY] A) x_1 h) (x, y).2) ∈
      U
⊢ ∀ (i : (↑(closure[tY] A) : Type u_5)),
    ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i (x, y).1,
        (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i (x, y).2) ∈
      U

Tactic:
rw [SetCoe.forall] at *

Premises used: SetCoe.forall
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S
hu : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : β) ↦ α) ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x y : β
hxy :
  ∀ (x_1 : Y) (h : x_1 ∈ A),
    ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) (Subtype.mk (p := fun (x : Y) ↦ x ∈ A) x_1 h) (x, y).1,
        (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) (Subtype.mk (p := fun (x : Y) ↦ x ∈ A) x_1 h) (x, y).2) ∈
      V
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
⊢ A ⊆ (fun (f : Y) ↦ (u f x, u f y)) ⁻¹' V

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

Premises used: Prod.mk
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S
hu : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : β) ↦ α) ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x y : β
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
hxy : A ⊆ (fun (f : Y) ↦ (u f x, u f y)) ⁻¹' V
⊢ ∀ (x_1 : Y) (h : x_1 ∈ closure[tY] A),
    ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) (Subtype.mk (p := fun (x : Y) ↦ x ∈ closure[tY] A) x_1 h)
          (x, y).1,
        (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A))
          (Subtype.mk (p := fun (x : Y) ↦ x ∈ closure[tY] A) x_1 h) (x, y).2) ∈
      U

Tactic:
(closure_minimal hxy <| hVclosed.preimage <| .prodMk ?_ ?_).trans (preimage_mono hVU)

Premises used: Set.Mem, closure_minimal, setOf, HasSubset.Subset.trans, Set.Subset, Set.preimage_mono, Set.preimage, IsClosed.preimage, Continuous.prodMk
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S
hu : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : β) ↦ α) ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x y : β
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
hxy : A ⊆ (fun (f : Y) ↦ (u f x, u f y)) ⁻¹' V
h : Continuous[tY, uα.toTopologicalSpace] fun (f : Y) ↦ u f x
h₁ : Continuous[tY, uα.toTopologicalSpace] fun (f : Y) ↦ u f y
⊢ ∀ (x_1 : Y) (h : x_1 ∈ closure[tY] A),
    ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) (Subtype.mk (p := fun (x : Y) ↦ x ∈ closure[tY] A) x_1 h)
          (x, y).1,
        (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A))
          (Subtype.mk (p := fun (x : Y) ↦ x ∈ closure[tY] A) x_1 h) (x, y).2) ∈
      U

Tactic:
refine (closure_minimal hxy <| hVclosed.preimage <| .prodMk ?_ ?_).trans (preimage_mono hVU)

Premises used: closure_minimal, HasSubset.Subset.trans, Set.preimage_mono, IsClosed.preimage, Continuous.prodMk
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S
hu : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : β) ↦ α) ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x y : β
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
hxy : A ⊆ (fun (f : Y) ↦ (u f x, u f y)) ⁻¹' V
⊢ Continuous[tY, uα.toTopologicalSpace] fun (f : Y) ↦ u f x

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

Premises used: Continuous.comp, continuous_apply, Set.restrict
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S
hu : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : β) ↦ α) ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x y : β
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
hxy : A ⊆ (fun (f : Y) ↦ (u f x, u f y)) ⁻¹' V
⊢ Continuous[tY, uα.toTopologicalSpace] fun (f : Y) ↦ u f x

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

Premises used: Continuous.comp, continuous_apply
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S
hu : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : β) ↦ α) ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x y : β
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
hxy : A ⊆ (fun (f : Y) ↦ (u f x, u f y)) ⁻¹' V
⊢ Continuous[tY, uα.toTopologicalSpace] fun (f : Y) ↦ u f y

Tactic:
(continuous_apply ⟨y, hyS⟩).comp hu

Premises used: Continuous.comp, continuous_apply, Set.restrict
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S
hu : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : β) ↦ α) ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x y : β
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
hxy : A ⊆ (fun (f : Y) ↦ (u f x, u f y)) ⁻¹' V
⊢ Continuous[tY, uα.toTopologicalSpace] fun (f : Y) ↦ u f y

Tactic:
exact (continuous_apply ⟨y, hyS⟩).comp hu

Premises used: Continuous.comp, continuous_apply
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
hA : UniformEquicontinuous (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A))
hu : Continuous[tY, Pi.topologicalSpace] u
rw :
  ∀ (hA : UniformEquicontinuousOn (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) univ)
    (hu : Continuous[tY, Pi.topologicalSpace] u),
    UniformEquicontinuousOn (ι := (↑(closure[tY] A) : Type u_5))
      (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) univ
⊢ UniformEquicontinuous (ι := (↑(closure[tY] A) : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A))

Tactic:
rw [← uniformEquicontinuousOn_univ] at hA ⊢

Premises used: uniformEquicontinuousOn_univ
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
hA : UniformEquicontinuousOn (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) univ
hu : Continuous[tY, Pi.topologicalSpace] u
⊢ UniformEquicontinuousOn (ι := (↑(closure[tY] A) : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A))
    univ

Tactic:
hA.closure' (Pi.continuous_restrict _ |>.comp hu)

Premises used: Continuous.comp, UniformEquicontinuousOn.closure', Pi.continuous_restrict