awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : IsUniformInducing u
this :
  IsUniformInducing (α := ι →ᵤ α) (β := ι →ᵤ γ)
    (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
      ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
⊢ UniformEquicontinuous F ↔ UniformEquicontinuous.{u_1, u_10, u_8} (α := γ) (β := β) ((fun (x : β → α) ↦ u ∘ x) ∘ F)
have simp : UniformContinuous (β := ι →ᵤ γ)
    (Function.comp (β := ι →ᵤ α)
      (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
        ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
      ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F)) ↔
  UniformContinuous (α := β) (β := ι →ᵤ γ)
    (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
      (swap (φ := fun (a : ι) (a_1 : β) ↦ γ) ((fun (x : β → α) ↦ u ∘ x) ∘ F)))
Tactic: simp only [uniformEquicontinuous_iff_uniformContinuous, this.uniformContinuous_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (hypothesis)
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
S : Set β
u : α → γ
hu : IsUniformInducing u
⊢ UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn.{u_1, u_10, u_8} (α := γ) ((fun (x : β → α) ↦ u ∘ x) ∘ F) S
have this : IsUniformInducing (α := ι →ᵤ α) (β := ι →ᵤ γ)
  (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
    ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
Tactic: have := UniformFun.postcomp_isUniformInducing (α := ι) hu
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
S : Set β
u : α → γ
hu : IsUniformInducing u
this :
  IsUniformInducing (α := ι →ᵤ α) (β := ι →ᵤ γ)
    (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
      ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
⊢ UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn.{u_1, u_10, u_8} (α := γ) ((fun (x : β → α) ↦ u ∘ x) ∘ F) S
have simp : UniformContinuousOn (β := ι →ᵤ γ)
    (Function.comp (β := ι →ᵤ α)
      (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
        ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
      ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F))
    S ↔
  UniformContinuousOn (β := ι →ᵤ γ)
    (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
      (swap (φ := fun (a : ι) (a_1 : β) ↦ γ) ((fun (x : β → α) ↦ u ∘ x) ∘ F)))
    S
Tactic: simp only [uniformEquicontinuousOn_iff_uniformContinuousOn, this.uniformContinuousOn_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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 ∈ 𝓤 α
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀,
    ∀ (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
have rcases : ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVclosed : IsClosed[instTopologicalSpaceProd] V) (hVU : V ⊆ U),
  ∀ᶠ (x : X) in 𝓝[S] x₀,
    ∀ (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: rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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) in 𝓝[S] x₀,
    ∀ (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
have h : ∀ (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) (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: filter_upwards [hA V hV, eventually_mem_nhdsWithin] with x hx hxS
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
⊢ ∀ (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
have 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
Tactic: rw [SetCoe.forall] at *
Cleared hypotheses: hx, hxS
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (hypothesis)
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
⊢ ∀ (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
have hx₁ : 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
have h : Continuous[tY, uα.toTopologicalSpace] fun (f : Y) ↦ u f x
Tactic: refine (closure_minimal hx <| hVclosed.preimage <| hu₂.prodMk ?_).trans (preimage_mono hVU)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
⊢ EquicontinuousAt (ι := (↑(closure[tY] A) : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) x₀
have 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₀
Tactic: rw [← equicontinuousWithinAt_univ] at hA ⊢
Cleared hypotheses: hA, hu
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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 ∈ 𝓤 α
⊢ ∀ᶠ (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
have 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
Tactic: rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
⊢ ∀ᶠ (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
have 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
Tactic: filter_upwards [hA V hV, mem_inf_of_right (mem_principal_self _)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
⊢ ∀ (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
have 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
Tactic: rw [SetCoe.forall] at *
Cleared hypotheses: hxy, hxS, hyS
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (hypothesis)
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
⊢ ∀ (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
have hxy₁ : 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
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
have h : Continuous[tY, uα.toTopologicalSpace] fun (f : Y) ↦ u f x
Tactic: refine (closure_minimal hxy <| hVclosed.preimage <| .prodMk ?_ ?_).trans (preimage_mono hVU)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
⊢ ∀ (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
have h₁ : Continuous[tY, uα.toTopologicalSpace] fun (f : Y) ↦ u f y
Tactic: refine (closure_minimal hxy <| hVclosed.preimage <| .prodMk ?_ ?_).trans (preimage_mono hVU)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
⊢ UniformEquicontinuous (ι := (↑(closure[tY] A) : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A))
have 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
Tactic: rw [← uniformEquicontinuousOn_univ] at hA ⊢
Cleared hypotheses: hA, hu
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : 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₀
have rcases : ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVU : ball (f x₀) V ⊆ U), f ⁻¹' U ∈ 𝓝[S] x₀
Tactic: rcases UniformSpace.mem_nhds_iff.mp hU with ⟨V, hV, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : 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₀
have rcases : ∀ (W : Set (α × α)) (hW : W ∈ 𝓤 α) (hWclosed : IsClosed[instTopologicalSpaceProd] W) (hWV : W ⊆ V), f ⁻¹' U ∈ 𝓝[S] x₀
Tactic: rcases mem_uniformity_isClosed hV with ⟨W, hW, hWclosed, hWV⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : 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[instTopologicalSpaceProd] W
hWV : W ⊆ V
⊢ f ⁻¹' U ∈ 𝓝[S] x₀
have h : ∀ (a : X),
  Membership.mem (γ := Set X)
    {x : X |
      Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ ∀ (i : ι), (F i x₀, F i x) ∈ W) x} x →
        Membership.mem (γ := Set X)
          {x : X | Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ x ∈ S) x} x → x ∈ f ⁻¹' U} x}
    a
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₂.prodMk_nhds (h₁ x hxS)) <|
    Eventually.of_forall hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : 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[instTopologicalSpaceProd] W
hWV : W ⊆ V
h :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X |
        Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ ∀ (i : ι), (F i x₀, F i x) ∈ W) x} x →
          Membership.mem (γ := Set X)
            {x : X | Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ x ∈ S) x} x → x ∈ f ⁻¹' U} x}
      a
⊢ f ⁻¹' U ∈ 𝓝[S] x₀
have h₄ : ∀ (a : X), (∀ (i : ι), (F i x₀, F i a) ∈ W) → a ∈ S → a ∈ f ⁻¹' U
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₂.prodMk_nhds (h₁ x hxS)) <|
    Eventually.of_forall hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst : l.NeBot
F : ι → X → α
f : X → α
x₀ : X
h₁ : Tendsto F l (𝓝 f)
h₂ : EquicontinuousAt F x₀
⊢ ContinuousAt f x₀
have rw : ∀ (h₁ : ∀ (x : X), Tendsto (fun (i : ι) ↦ F i x) l (𝓝 (f x))) (h₂ : EquicontinuousWithinAt F univ x₀),
  ContinuousWithinAt f univ x₀
Tactic: rw [← continuousWithinAt_univ, ← equicontinuousWithinAt_univ, tendsto_pi_nhds] at *
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst : l.NeBot
F : ι → β → α
f : β → α
S : Set β
h₁ : ∀ x ∈ S, Tendsto (fun (x_1 : ι) ↦ F x_1 x) l (𝓝 (f x))
h₂ : UniformEquicontinuousOn F S
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ (fun (x : β × β) ↦ (f x.1, f x.2)) ⁻¹' U ∈ 𝓤 β ⊓ 𝓟 (S ×ˢ S)
have rcases : ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVclosed : IsClosed[instTopologicalSpaceProd] V) (hVU : V ⊆ U),
  (fun (x : β × β) ↦ (f x.1, f x.2)) ⁻¹' U ∈ 𝓤 β ⊓ 𝓟 (S ×ˢ S)
Tactic: rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst : l.NeBot
F : ι → β → α
f : β → α
S : Set β
h₁ : ∀ x ∈ S, Tendsto (fun (x_1 : ι) ↦ F x_1 x) l (𝓝 (f x))
h₂ : UniformEquicontinuousOn F S
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
⊢ (fun (x : β × β) ↦ (f x.1, f x.2)) ⁻¹' U ∈ 𝓤 β ⊓ 𝓟 (S ×ˢ S)
have h : ∀ (a : β × β),
  (∀ (i : ι), (F i a.1, F i a.2) ∈ V) →
    a ∈ S ×ˢ S → Membership.mem (γ := Set (β × β)) ((fun (x : β × β) ↦ (f x.1, f x.2)) ⁻¹' U) a
Tactic: filter_upwards [h₂ V hV, mem_inf_of_right (mem_principal_self _)]