awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact hA.closure' (Pi.continuous_restrict _ |>.comp hu)

Premises used: Continuous.comp, UniformEquicontinuousOn.closure', Pi.continuous_restrict
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
A : Set (β → α)
hA : A.UniformEquicontinuous
⊢ (closure[Pi.topologicalSpace] A).UniformEquicontinuous

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

Premises used: Set.Mem, UniformEquicontinuous.closure', continuous_id
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
A : Set (β → α)
S : Set β
hA : A.UniformEquicontinuousOn S
⊢ (closure[Pi.topologicalSpace] A).UniformEquicontinuousOn S

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

Premises used: Set.Mem, UniformEquicontinuousOn.closure', Pi.continuous_restrict
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
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₀)
rcases : ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVU : ball (f x₀) V ⊆ U), f ⁻¹' U ∈ 𝓝[S] x₀
⊢ f ⁻¹' U ∈ 𝓝[S] x₀

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

Premises used: UniformSpace.mem_nhds_iff, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
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
rcases :
  ∀ (W : Set (α × α)) (hW : W ∈ 𝓤 α) (hWclosed : IsClosed[instTopologicalSpaceProd] W) (hWV : W ⊆ V), f ⁻¹' U ∈ 𝓝[S] x₀
⊢ f ⁻¹' U ∈ 𝓝[S] x₀

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

Premises used: mem_uniformity_isClosed
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
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
x : X
hx : ∀ (i : ι), (F i x₀, F i x) ∈ W
hxS : x ∈ S
⊢ x ∈ f ⁻¹' U

Tactic:
hVU <| ball_mono hWV (f x₀) <| hWclosed.mem_of_tendsto (h₂.prodMk_nhds (h₁ x hxS)) <|
    Eventually.of_forall hx

Premises used: Set.Mem, UniformSpace.ball_mono, setOf, IsClosed.mem_of_tendsto, Filter.Eventually.of_forall, Set.preimage, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
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
h₄ h₅ : ∀ (x : X) (hx : ∀ (i : ι), (F i x₀, F i x) ∈ W) (hxS : x ∈ S), x ∈ f ⁻¹' U
⊢ 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₂.prodMk_nhds (h₁ x hxS)) <|
    Eventually.of_forall hx

Premises used: eventually_mem_nhdsWithin, UniformSpace.ball_mono
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
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₀
rw :
  ∀ (h₁ : ∀ (x : X), Tendsto (fun (i : ι) ↦ F i x) l (𝓝 (f x))) (h₂ : EquicontinuousWithinAt F univ x₀),
    ContinuousWithinAt f univ x₀
⊢ ContinuousAt f x₀

Tactic:
rw [← continuousWithinAt_univ, ← equicontinuousWithinAt_univ, tendsto_pi_nhds] at *

Premises used: continuousWithinAt_univ, tendsto_pi_nhds, equicontinuousWithinAt_univ
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
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₁ : ∀ (x : X), Tendsto (fun (i : ι) ↦ F i x) l (𝓝 (f x))
h₂ : EquicontinuousWithinAt F univ x₀
⊢ ContinuousWithinAt f univ x₀

Tactic:
continuousWithinAt_of_equicontinuousWithinAt (fun x _ ↦ h₁ x) (h₁ x₀) h₂

Premises used: Filter.Tendsto.continuousWithinAt_of_equicontinuousWithinAt
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
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₁ : ∀ (x : X), Tendsto (fun (i : ι) ↦ F i x) l (𝓝 (f x))
h₂ : EquicontinuousWithinAt F univ x₀
⊢ ContinuousWithinAt f univ x₀

Tactic:
exact continuousWithinAt_of_equicontinuousWithinAt (fun x _ ↦ h₁ x) (h₁ x₀) h₂

Premises used: Filter.Tendsto.continuousWithinAt_of_equicontinuousWithinAt
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
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 → α
h₁ : Tendsto F l (𝓝 f)
h₂ : Equicontinuous F
⊢ Continuous[tX, uα.toTopologicalSpace] f

Tactic:
continuous_iff_continuousAt.mpr fun x => h₁.continuousAt_of_equicontinuousAt (h₂ x)

Premises used: Iff.mpr, Filter.Tendsto.continuousAt_of_equicontinuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
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
h₁ : ∀ x ∈ S, Tendsto (fun (x_1 : ι) ↦ F x_1 x) l (𝓝 (f x))
h₂ : EquicontinuousOn F S
⊢ ContinuousOn f S

Tactic:
fun x hx ↦ Filter.Tendsto.continuousWithinAt_of_equicontinuousWithinAt h₁ (h₁ x hx) (h₂ x hx)

Premises used: Filter.Tendsto.continuousWithinAt_of_equicontinuousWithinAt, ContinuousOn
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
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 ∈ 𝓤 α
rcases :
  ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVclosed : IsClosed[instTopologicalSpaceProd] V) (hVU : V ⊆ U),
    (fun (x : β × β) ↦ (f x.1, f x.2)) ⁻¹' U ∈ 𝓤 β ⊓ 𝓟 (S ×ˢ S)
⊢ (fun (x : β × β) ↦ (f x.1, f x.2)) ⁻¹' U ∈ 𝓤 β ⊓ 𝓟 (S ×ˢ S)

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

Premises used: mem_uniformity_isClosed
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
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
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
⊢ (fun (x : β × β) ↦ (f x.1, f x.2)) ⁻¹' U ∈ 𝓤 β ⊓ 𝓟 (S ×ˢ S)

Tactic:
filter_upwards [h₂ 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:
ι : 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
x y : β
hxy : ∀ (i : ι), (F i (x, y).1, F i (x, y).2) ∈ V
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
⊢ Membership.mem (γ := Set (β × β)) ((fun (x : β × β) ↦ (f x.1, f x.2)) ⁻¹' U) (x, y)

Tactic:
hVU <| hVclosed.mem_of_tendsto ((h₁ x hxS).prodMk_nhds (h₁ y hyS)) <|
    Eventually.of_forall hxy

Premises used: Set.Mem, setOf, IsClosed.mem_of_tendsto, Filter.Eventually.of_forall, Set.preimage, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
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
x y : β
hxy : ∀ (i : ι), (F i (x, y).1, F i (x, y).2) ∈ V
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
⊢ Membership.mem (γ := Set (β × β)) ((fun (x : β × β) ↦ (f x.1, f x.2)) ⁻¹' U) (x, y)

Tactic:
exact hVU <| hVclosed.mem_of_tendsto ((h₁ x hxS).prodMk_nhds (h₁ y hyS)) <|
    Eventually.of_forall hxy

Premises used: IsClosed.mem_of_tendsto, Filter.Eventually.of_forall, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst : l.NeBot
F : ι → β → α
f : β → α
h₁ : Tendsto F l (𝓝 f)
h₂ : UniformEquicontinuous F
rw :
  ∀ (h₁ : ∀ (x : β), Tendsto (fun (i : ι) ↦ F i x) l (𝓝 (f x))) (h₂ : UniformEquicontinuousOn F univ),
    UniformContinuousOn f univ
⊢ UniformContinuous f

Tactic:
rw [← uniformContinuousOn_univ, ← uniformEquicontinuousOn_univ, tendsto_pi_nhds] at *

Premises used: uniformEquicontinuousOn_univ, uniformContinuousOn_univ, tendsto_pi_nhds
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst : l.NeBot
F : ι → β → α
f : β → α
h₁ : ∀ (x : β), Tendsto (fun (i : ι) ↦ F i x) l (𝓝 (f x))
h₂ : UniformEquicontinuousOn F univ
⊢ UniformContinuousOn f univ

Tactic:
uniformContinuousOn_of_uniformEquicontinuousOn (fun x _ ↦ h₁ x) h₂

Premises used: Filter.Tendsto.uniformContinuousOn_of_uniformEquicontinuousOn
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst : l.NeBot
F : ι → β → α
f : β → α
h₁ : ∀ (x : β), Tendsto (fun (i : ι) ↦ F i x) l (𝓝 (f x))
h₂ : UniformEquicontinuousOn F univ
⊢ UniformContinuousOn f univ

Tactic:
exact uniformContinuousOn_of_uniformEquicontinuousOn (fun x _ ↦ h₁ x) h₂

Premises used: Filter.Tendsto.uniformContinuousOn_of_uniformEquicontinuousOn
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : 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[tX] s
rw :
  ∀ (hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id i} (f x))
    (hs : ∀ y ∈ s, Tendsto (fun (x : ι) ↦ F x y) l (𝓝 (f y))) (hx : x ∈ closure[tX] s),
    ∀ i ∈ 𝓤 α, ∀ᶠ (x_1 : ι) in l, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id i} (F x_1 x)
⊢ Tendsto (fun (x_1 : ι) ↦ F x_1 x) l (𝓝 z)

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

Premises used: uniformity, Filter.basis_sets, Filter.HasBasis.tendsto_right_iff, nhds_basis_uniformity
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : 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, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id i} (f x)
hs : ∀ y ∈ s, Tendsto (fun (x : ι) ↦ F x y) l (𝓝 (f y))
hx : x ∈ closure[tX] s
U : Set (α × α)
hU : U ∈ 𝓤 α
rcases :
  ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVs : SetRel.IsSymm V) (hVU : (SetRel.comp V V).comp V ⊆ U),
    ∀ᶠ (x_1 : ι) in l, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id U} (F x_1 x)
⊢ ∀ᶠ (x_1 : ι) in l, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id U} (F x_1 x)

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

Premises used: comp_comp_symm_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : 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, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id i} (f x)
hs : ∀ y ∈ s, Tendsto (fun (x : ι) ↦ F x y) l (𝓝 (f y))
hx : x ∈ closure[tX] s
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
rw :
  ∀ (hx : (𝓝[s] x).NeBot) (U : Set (α × α)) (hU : U ∈ 𝓤 α) (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVs : SetRel.IsSymm V)
    (hVU : (SetRel.comp V V).comp V ⊆ U),
    ∀ᶠ (x_1 : ι) in l, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id U} (F x_1 x)
⊢ ∀ᶠ (x_1 : ι) in l, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id U} (F x_1 x)

Tactic:
rw [mem_closure_iff_nhdsWithin_neBot] at hx

Premises used: mem_closure_iff_nhdsWithin_neBot
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : 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, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id i} (f x)
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 : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
⊢ ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V

Tactic:
have : ∀ᶠ y in 𝓝[s] x, y ∈ s ∧ (∀ i, (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V :=
    eventually_mem_nhdsWithin.and <| ((hF V hV).filter_mono nhdsWithin_le_nhds).and (hf V hV)
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : 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, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id i} (f x)
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 : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
this : ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V
rcases :
  ∀ (y : X) (hys : y ∈ s) (hFy : ∀ (i : ι), (F i x, F i y) ∈ V) (hfy : (f y, z) ∈ V),
    ∀ᶠ (x_1 : ι) in l, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id U} (F x_1 x)
⊢ ∀ᶠ (x_1 : ι) in l, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id U} (F x_1 x)

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

Premises used: Filter.Eventually.exists
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : 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, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id i} (f x)
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 : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp 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
h : ∀ (i : ι) (hi : Membership.mem (γ := Set ι) ((fun (x : ι) ↦ F x y) ⁻¹' ball (f y) V) i), (F i x, z) ∈ id U
⊢ ∀ᶠ (x_1 : ι) in l, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id U} (F x_1 x)

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

Premises used: UniformSpace.ball_mem_nhds
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : 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, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id i} (f x)
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 : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp 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 : Membership.mem (γ := Set ι) ((fun (x : ι) ↦ F x y) ⁻¹' ball (f y) V) i
⊢ (F i x, z) ∈ id U

Tactic:
hVU ⟨_, ⟨_, hFy i, mem_ball_symmetry.2 hi⟩, hfy⟩

Premises used: Iff.mpr, Set.Mem, UniformSpace.mem_ball_symmetry, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : 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, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id i} (f x)
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 : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp 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 : Membership.mem (γ := Set ι) ((fun (x : ι) ↦ F x y) ⁻¹' ball (f y) V) i
⊢ (F i x, z) ∈ id U

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

Premises used: Iff.mpr, UniformSpace.mem_ball_symmetry, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
hF : Equicontinuous F
hf : Continuous[tX, uα.toTopologicalSpace] f
⊢ IsClosed[tX] {x : X | Tendsto (fun (x_1 : ι) ↦ F x_1 x) l (𝓝 (f x))}

Tactic:
closure_subset_iff_isClosed.mp fun x hx ↦
    (hF x).tendsto_of_mem_closure (hf.continuousAt.mono_left inf_le_left) (fun _ ↦ id) hx

Premises used: EquicontinuousAt.tendsto_of_mem_closure, closure_subset_iff_isClosed, id, Continuous.continuousAt, Iff.mp, Filter.Tendsto.mono_left, inf_le_left
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
e : α ≃ β
h₁ : UniformContinuous e.toFun
h₂ : UniformContinuous e.invFun
e' : α ≃ β
h₁' : UniformContinuous e'.toFun
h₂' : UniformContinuous e'.invFun
h :
  { toEquiv := e, uniformContinuous_toFun := h₁, uniformContinuous_invFun := h₂ : α ≃ᵤ β }.toEquiv =
    { toEquiv := e', uniformContinuous_toFun := h₁', uniformContinuous_invFun := h₂' : α ≃ᵤ β }.toEquiv
⊢ { toEquiv := e, uniformContinuous_toFun := h₁, uniformContinuous_invFun := h₂ : α ≃ᵤ β } =
    { toEquiv := e', uniformContinuous_toFun := h₁', uniformContinuous_invFun := h₂' }

Tactic:
simpa only [mk.injEq]

Premises used: UniformEquiv.mk.injEq
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
a : α ≃ β
b : UniformContinuous a.toFun
c : UniformContinuous a.invFun
⊢ Eq (α := (a : α) → β)
    (⇑{ toEquiv := a, uniformContinuous_toFun := b, uniformContinuous_invFun := c : α ≃ᵤ β } : (a : α) → β)
    (⇑a : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
⊢ Eq (α := (a : α) → β) (⇑h.toEquiv : (a : α) → β) (⇑h : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
⊢ Eq (α := (a : β) → α) (⇑h.symm : (a : β) → α) (⇑h.symm : (a : β) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h h' : α ≃ᵤ β
H : ∀ (x : α), Eq.{u_1 + 1} (α := β) ((h : (a : α) → β) x : β) ((h' : (a : α) → β) x : β)
⊢ h = h'

Tactic:
toEquiv_injective <| Equiv.ext H

Premises used: Equiv.ext, UniformEquiv.toEquiv_injective
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
γ : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
h₁ : α ≃ᵤ β
h₂ : β ≃ᵤ γ
a : α
⊢ Eq.{u_2 + 1} (α := γ) ((h₁.trans h₂ : (a : α) → γ) a : γ) ((h₂ : (a : β) → γ) ((h₁ : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
a : α ≃ β
b : UniformContinuous a.toFun
c : UniformContinuous a.invFun
⊢ Eq (α := (a : β) → α)
    (⇑{ toEquiv := a, uniformContinuous_toFun := b, uniformContinuous_invFun := c : α ≃ᵤ β }.symm : (a : β) → α)
    (⇑a.symm : (a : β) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
inst : UniformSpace α
⊢ Eq (α := α ≃ᵤ α) (UniformEquiv.symm (UniformEquiv.refl α)) (UniformEquiv.refl α)

Tactic:
rfl

Premises used: UniformEquiv.symm, UniformEquiv.refl, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
⊢ UniformContinuous.{u, u_1} (α := α) (β := β) (⇑h : (a : α) → β)

Tactic:
h.uniformContinuous_toFun

Premises used: UniformEquiv.uniformContinuous_toFun
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
⊢ Continuous.{u, u_1} (X := α) (Y := β) (⇑h : (a : α) → β)

Tactic:
h.uniformContinuous.continuous

Premises used: UniformContinuous.continuous, UniformEquiv.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
⊢ UniformContinuous.{u_1, u} (α := β) (β := α) (⇑h.symm : (a : β) → α)

Tactic:
h.uniformContinuous_invFun

Premises used: UniformEquiv.uniformContinuous_invFun
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
h : α ≃ᵤ β
⊢ Continuous.{u_1, u} (X := β) (Y := α) (⇑h.symm : (a : β) → α)

Tactic:
h.uniformContinuous_symm.continuous

Premises used: UniformEquiv.uniformContinuous_symm, UniformContinuous.continuous
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
e : α ≃ᵤ β
⊢ Eq (α := (a : α) → β) (⇑e.toHomeomorph : (a : α) → β) (⇑e : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.Equiv
Goal:
α : Type u
β : Type u_1
inst : UniformSpace α
inst_1 : UniformSpace β
e : α ≃ᵤ β
⊢ Eq (α := (a : β) → α) (⇑e.toHomeomorph.symm : (a : β) → α) (⇑e.symm : (a : β) → α)

Tactic:
rfl

Premises used: rfl