awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
inst : Finite ι
F : ι → X → α
S : Set X
x₀ : X
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ (i : ι), ContinuousWithinAt (F i) S x₀

Tactic:
simp [EquicontinuousWithinAt, ContinuousWithinAt,
    (nhds_basis_uniformity' (𝓤 α).basis_sets).tendsto_right_iff, UniformSpace.ball,
    @forall_comm _ ι]

Premises used: ContinuousWithinAt, EquicontinuousWithinAt, nhds_basis_uniformity', uniformity, forall_comm, UniformSpace.ball, Filter.basis_sets, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
inst : Finite ι
F : ι → X → α
⊢ Equicontinuous F ↔ ∀ (i : ι), Continuous[tX, uα.toTopologicalSpace] (F i)

Tactic:
simp only [Equicontinuous, equicontinuousAt_finite, continuous_iff_continuousAt, @forall_comm ι]

Premises used: Equicontinuous, forall_comm, equicontinuousAt_finite, continuous_iff_continuousAt
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
inst : Finite ι
F : ι → X → α
S : Set X
⊢ EquicontinuousOn F S ↔ ∀ (i : ι), ContinuousOn (F i) S

Tactic:
simp only [EquicontinuousOn, equicontinuousWithinAt_finite, ContinuousOn, @forall_comm ι]

Premises used: forall_comm, equicontinuousWithinAt_finite, EquicontinuousOn, ContinuousOn
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst : Finite ι
F : ι → β → α
simp :
  (∀ (b : ι) (a : Set (α × α)) (a_1 : a ∈ 𝓤 α), ∀ᶠ (x : β × β) in 𝓤 β, (F b x.1, F b x.2) ∈ a) ↔
    ∀ (i : ι), UniformContinuous (F i)
⊢ UniformEquicontinuous F ↔ ∀ (i : ι), UniformContinuous (F i)

Tactic:
simp only [UniformEquicontinuous, eventually_all, @forall_comm _ ι]

Premises used: forall_comm, Filter.eventually_all, UniformEquicontinuous
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst : Finite ι
F : ι → β → α
⊢ (∀ (b : ι) (a : Set (α × α)) (a_1 : a ∈ 𝓤 α), ∀ᶠ (x : β × β) in 𝓤 β, (F b x.1, F b x.2) ∈ a) ↔
    ∀ (i : ι), UniformContinuous (F i)

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst : Finite ι
F : ι → β → α
S : Set β
simp :
  (∀ (b : ι) (a : Set (α × α)) (a_1 : a ∈ 𝓤 α), ∀ᶠ (x : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), (F b x.1, F b x.2) ∈ a) ↔
    ∀ (i : ι), UniformContinuousOn (F i) S
⊢ UniformEquicontinuousOn F S ↔ ∀ (i : ι), UniformContinuousOn (F i) S

Tactic:
simp only [UniformEquicontinuousOn, eventually_all, @forall_comm _ ι]

Premises used: forall_comm, Filter.eventually_all, UniformEquicontinuousOn
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst : Finite ι
F : ι → β → α
S : Set β
⊢ (∀ (b : ι) (a : Set (α × α)) (a_1 : a ∈ 𝓤 α), ∀ᶠ (x : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), (F b x.1, F b x.2) ∈ a) ↔
    ∀ (i : ι), UniformContinuousOn (F i) S

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
inst : Unique ι
F : ι → X → α
x : X
⊢ EquicontinuousAt F x ↔ ContinuousAt (F default) x

Tactic:
equicontinuousAt_finite.trans Unique.forall_iff

Premises used: Unique.forall_iff, Iff.trans, equicontinuousAt_finite
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
inst : Unique ι
F : ι → X → α
S : Set X
x : X
⊢ EquicontinuousWithinAt F S x ↔ ContinuousWithinAt (F default) S x

Tactic:
equicontinuousWithinAt_finite.trans Unique.forall_iff

Premises used: Unique.forall_iff, equicontinuousWithinAt_finite, Iff.trans
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
inst : Unique ι
F : ι → X → α
⊢ Equicontinuous F ↔ Continuous[tX, uα.toTopologicalSpace] (F default)

Tactic:
equicontinuous_finite.trans Unique.forall_iff

Premises used: equicontinuous_finite, Unique.forall_iff, Iff.trans
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
inst : Unique ι
F : ι → X → α
S : Set X
⊢ EquicontinuousOn F S ↔ ContinuousOn (F default) S

Tactic:
equicontinuousOn_finite.trans Unique.forall_iff

Premises used: Unique.forall_iff, Iff.trans, equicontinuousOn_finite
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst : Unique ι
F : ι → β → α
⊢ UniformEquicontinuous F ↔ UniformContinuous (F default)

Tactic:
uniformEquicontinuous_finite.trans Unique.forall_iff

Premises used: Unique.forall_iff, Iff.trans, uniformEquicontinuous_finite
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst : Unique ι
F : ι → β → α
S : Set β
⊢ UniformEquicontinuousOn F S ↔ UniformContinuousOn (F default) S

Tactic:
uniformEquicontinuousOn_finite.trans Unique.forall_iff

Premises used: Unique.forall_iff, Iff.trans, uniformEquicontinuousOn_finite
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
mp : EquicontinuousWithinAt F S x₀ → ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
mpr : (∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U) → EquicontinuousWithinAt F S x₀
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : EquicontinuousWithinAt F S x₀
U : Set (α × α)
hU : U ∈ 𝓤 α
mp :
  ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVsymm : SetRel.IsSymm V) (hVU : SetRel.comp V V ⊆ U),
    ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
⊢ ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
rcases comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVsymm, hVU⟩

Premises used: 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 α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : EquicontinuousWithinAt F S x₀
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
⊢ ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
⟨_, H V hV, fun x hx y hy i => hVU (SetRel.prodMk_mem_comp ?_ (hy i))⟩

Premises used: And.intro, Exists.intro, SetRel.prodMk_mem_comp
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : EquicontinuousWithinAt F S x₀
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
mp :
  ∀ (x : X) (hx : Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ ∀ (i : ι), (F i x₀, F i x) ∈ V) x} x) (y : X)
    (hy : Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ ∀ (i : ι), (F i x₀, F i x) ∈ V) x} y) (i : ι),
    (F i x, F i x₀) ∈ V
⊢ ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
refine ⟨_, H V hV, fun x hx y hy i => hVU (SetRel.prodMk_mem_comp ?_ (hy i))⟩
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : EquicontinuousWithinAt F S x₀
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
x : X
hx : Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ ∀ (i : ι), (F i x₀, F i x) ∈ V) x} x
y : X
hy : Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ ∀ (i : ι), (F i x₀, F i x) ∈ V) x} y
i : ι
⊢ (F i x, F i x₀) ∈ V

Tactic:
SetRel.symm V (hx i)

Premises used: SetRel.symm
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : EquicontinuousWithinAt F S x₀
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
x : X
hx : Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ ∀ (i : ι), (F i x₀, F i x) ∈ V) x} x
y : X
hy : Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ ∀ (i : ι), (F i x₀, F i x) ∈ V) x} y
i : ι
⊢ (F i x, F i x₀) ∈ V

Tactic:
exact SetRel.symm V (hx i)

Premises used: SetRel.symm
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
U : Set (α × α)
hU : U ∈ 𝓤 α
mpr :
  ∀ (V : Set X) (hV : V ∈ 𝓝[S] x₀) (hVU : ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U),
    ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U

Tactic:
rcases H U hU with ⟨V, hV, hVU⟩
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set X
hV : V ∈ 𝓝[S] x₀
hVU : ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
⊢ ∀ a ∈ V, ∀ (i : ι), (F i x₀, F i a) ∈ U

Tactic:
fun x hx i => hVU x₀ (mem_of_mem_nhdsWithin hx₀ hV) x hx i

Premises used: mem_of_mem_nhdsWithin
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set X
hV : V ∈ 𝓝[S] x₀
hVU : ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
h :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X | x ∈ V → Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ ∀ (i : ι), (F i x₀, F i x) ∈ U) x} x} a
h₁ : ∀ a ∈ V, ∀ (i : ι), (F i x₀, F i a) ∈ U
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U

Tactic:
filter_upwards [hV] using fun x hx i => hVU x₀ (mem_of_mem_nhdsWithin hx₀ hV) x hx i

Premises used: mem_of_mem_nhdsWithin
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
simp_rw : EquicontinuousWithinAt F univ x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
simp_rw₁ :
  (∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[univ] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U) ↔
    ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
⊢ EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
simp_rw [← equicontinuousWithinAt_univ, equicontinuousWithinAt_iff_pair (mem_univ x₀),
    nhdsWithin_univ]

Premises used: nhdsWithin_univ, equicontinuousWithinAt_iff_pair, equicontinuousWithinAt_univ, Set.mem_univ
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
h : UniformEquicontinuous F
⊢ Equicontinuous F

Tactic:
fun x₀ U hU ↦
  mem_of_superset (ball_mem_nhds x₀ (h U hU)) fun _ hx i ↦ hx i

Premises used: Equicontinuous, UniformSpace.ball_mem_nhds, Filter.Eventually, EquicontinuousAt, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
h : UniformEquicontinuousOn F S
⊢ EquicontinuousOn F S

Tactic:
fun _ hx₀ U hU ↦
  mem_of_superset (ball_mem_nhdsWithin hx₀ (h U hU)) fun _ hx i ↦ hx i

Premises used: EquicontinuousWithinAt, Filter.Eventually, EquicontinuousOn, UniformSpace.ball_mem_nhdsWithin, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
h : EquicontinuousAt F x₀
i : ι
⊢ ContinuousAt (F i) x₀

Tactic:
(UniformSpace.hasBasis_nhds _).tendsto_right_iff.2 fun U ⟨hU, _⟩ ↦ (h U hU).mono fun _x hx ↦ hx i

Premises used: Iff.mpr, ContinuousAt, Filter.Eventually, _private.0.EquicontinuousAt.continuousAt.match_1, Membership.mem, nhds, UniformSpace.ball, UniformSpace.hasBasis_nhds, Filter.Eventually.mono, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
h : EquicontinuousWithinAt F S x₀
i : ι
⊢ ContinuousWithinAt (F i) S x₀

Tactic:
(UniformSpace.hasBasis_nhds _).tendsto_right_iff.2 fun U ⟨hU, _⟩ ↦ (h U hU).mono fun _x hx ↦ hx i

Premises used: Iff.mpr, ContinuousWithinAt, nhdsWithin, Filter.Eventually, _private.0.EquicontinuousAt.continuousAt.match_1, Membership.mem, UniformSpace.ball, UniformSpace.hasBasis_nhds, Filter.Eventually.mono, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
H : Set (X → α)
x₀ : X
h : H.EquicontinuousAt x₀
f : X → α
hf : f ∈ H
⊢ ContinuousAt f x₀

Tactic:
h.continuousAt ⟨f, hf⟩

Premises used: Subtype.mk, EquicontinuousAt.continuousAt
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
H : Set (X → α)
S : Set X
x₀ : X
h : H.EquicontinuousWithinAt S x₀
f : X → α
hf : f ∈ H
⊢ ContinuousWithinAt f S x₀

Tactic:
h.continuousWithinAt ⟨f, hf⟩

Premises used: EquicontinuousWithinAt.continuousWithinAt, Subtype.mk
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
h : Equicontinuous F
i : ι
⊢ Continuous[tX, uα.toTopologicalSpace] (F i)

Tactic:
continuous_iff_continuousAt.mpr fun x => (h x).continuousAt i

Premises used: Iff.mpr, EquicontinuousAt.continuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
h : EquicontinuousOn F S
i : ι
⊢ ContinuousOn (F i) S

Tactic:
fun x hx ↦ (h x hx).continuousWithinAt i

Premises used: EquicontinuousWithinAt.continuousWithinAt, ContinuousOn
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
H : Set (X → α)
h : H.Equicontinuous
f : X → α
hf : f ∈ H
⊢ Continuous[tX, uα.toTopologicalSpace] f

Tactic:
h.continuous ⟨f, hf⟩

Premises used: Equicontinuous.continuous, Subtype.mk
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
H : Set (X → α)
S : Set X
h : H.EquicontinuousOn S
f : X → α
hf : f ∈ H
⊢ ContinuousOn f S

Tactic:
h.continuousOn ⟨f, hf⟩

Premises used: Subtype.mk, EquicontinuousOn.continuousOn
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
h : UniformEquicontinuous F
i : ι
⊢ UniformContinuous (F i)

Tactic:
fun U hU =>
  mem_map.mpr (mem_of_superset (h U hU) fun _ hxy => hxy i)

Premises used: Iff.mpr, UniformContinuous, Filter.Tendsto, Filter.mem_map, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
h : UniformEquicontinuousOn F S
i : ι
⊢ UniformContinuousOn (F i) S

Tactic:
fun U hU =>
  mem_map.mpr (mem_of_superset (h U hU) fun _ hxy => hxy i)

Premises used: Iff.mpr, Filter.Tendsto, UniformContinuousOn, Filter.mem_map, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
H : Set (β → α)
h : H.UniformEquicontinuous
f : β → α
hf : f ∈ H
⊢ UniformContinuous f

Tactic:
h.uniformContinuous ⟨f, hf⟩

Premises used: UniformEquicontinuous.uniformContinuous, Subtype.mk
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
H : Set (β → α)
S : Set β
h : H.UniformEquicontinuousOn S
f : β → α
hf : f ∈ H
⊢ UniformContinuousOn f S

Tactic:
h.uniformContinuousOn ⟨f, hf⟩

Premises used: Subtype.mk, UniformEquicontinuousOn.uniformContinuousOn
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
h : EquicontinuousAt F x₀
u : κ → ι
⊢ EquicontinuousAt (F ∘ u) x₀

Tactic:
fun U hU => (h U hU).mono fun _ H k => H (u k)

Premises used: Filter.Eventually.mono, EquicontinuousAt
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
h : EquicontinuousWithinAt F S x₀
u : κ → ι
⊢ EquicontinuousWithinAt (F ∘ u) S x₀

Tactic:
fun U hU ↦ (h U hU).mono fun _ H k => H (u k)

Premises used: EquicontinuousWithinAt, Filter.Eventually.mono
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
H H' : Set (X → α)
x₀ : X
h : H.EquicontinuousAt x₀
hH : H' ⊆ H
⊢ H'.EquicontinuousAt x₀

Tactic:
h.comp (inclusion hH)

Premises used: EquicontinuousAt.comp, Set.inclusion
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
H H' : Set (X → α)
S : Set X
x₀ : X
h : H.EquicontinuousWithinAt S x₀
hH : H' ⊆ H
⊢ H'.EquicontinuousWithinAt S x₀

Tactic:
h.comp (inclusion hH)

Premises used: Set.inclusion, EquicontinuousWithinAt.comp
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
h : Equicontinuous F
u : κ → ι
⊢ Equicontinuous (F ∘ u)

Tactic:
fun x => (h x).comp u

Premises used: Equicontinuous, EquicontinuousAt.comp
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
h : EquicontinuousOn F S
u : κ → ι
⊢ EquicontinuousOn (F ∘ u) S

Tactic:
fun x hx ↦ (h x hx).comp u

Premises used: EquicontinuousOn, EquicontinuousWithinAt.comp
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
H H' : Set (X → α)
h : H.Equicontinuous
hH : H' ⊆ H
⊢ H'.Equicontinuous

Tactic:
h.comp (inclusion hH)

Premises used: Equicontinuous.comp, Set.inclusion
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
H H' : Set (X → α)
S : Set X
h : H.EquicontinuousOn S
hH : H' ⊆ H
⊢ H'.EquicontinuousOn S

Tactic:
h.comp (inclusion hH)

Premises used: Set.inclusion, EquicontinuousOn.comp
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
h : UniformEquicontinuous F
u : κ → ι
⊢ UniformEquicontinuous (F ∘ u)

Tactic:
fun U hU => (h U hU).mono fun _ H k => H (u k)

Premises used: Filter.Eventually.mono, UniformEquicontinuous
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
h : UniformEquicontinuousOn F S
u : κ → ι
⊢ UniformEquicontinuousOn (F ∘ u) S

Tactic:
fun U hU ↦ (h U hU).mono fun _ H k => H (u k)

Premises used: UniformEquicontinuousOn, Filter.Eventually.mono
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
H H' : Set (β → α)
h : H.UniformEquicontinuous
hH : H' ⊆ H
⊢ H'.UniformEquicontinuous

Tactic:
h.comp (inclusion hH)

Premises used: UniformEquicontinuous.comp, Set.inclusion
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
H H' : Set (β → α)
S : Set β
h : H.UniformEquicontinuousOn S
hH : H' ⊆ H
⊢ H'.UniformEquicontinuousOn S

Tactic:
h.comp (inclusion hH)

Premises used: UniformEquicontinuousOn.comp, Set.inclusion
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔
    EquicontinuousAt (ι := { x : X → α // x ∈ range F }) (Subtype.val (p := fun (x : X → α) ↦ x ∈ range F)) x₀

Tactic:
simp only [EquicontinuousAt, forall_subtype_range_iff]

Premises used: EquicontinuousAt, Set.forall_subtype_range_iff
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
⊢ EquicontinuousWithinAt F S x₀ ↔
    EquicontinuousWithinAt (ι := { x : X → α // x ∈ range F }) (Subtype.val (p := fun (x : X → α) ↦ x ∈ range F)) S x₀

Tactic:
simp only [EquicontinuousWithinAt, forall_subtype_range_iff]

Premises used: EquicontinuousWithinAt, Set.forall_subtype_range_iff
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
⊢ Equicontinuous F ↔
    Equicontinuous (ι := { x : X → α // x ∈ range F }) (Subtype.val (p := fun (x : X → α) ↦ x ∈ range F))

Tactic:
forall_congr' fun _ => equicontinuousAt_iff_range

Premises used: Equicontinuous, equicontinuousAt_iff_range, forall_congr'
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
⊢ EquicontinuousOn F S ↔
    EquicontinuousOn (ι := { x : X → α // x ∈ range F }) (Subtype.val (p := fun (x : X → α) ↦ x ∈ range F)) S

Tactic:
forall_congr' fun _ ↦ forall_congr' fun _ ↦ equicontinuousWithinAt_iff_range

Premises used: equicontinuousWithinAt_iff_range, EquicontinuousOn, forall_congr'
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
h : UniformEquicontinuous F
rw : UniformEquicontinuous (F ∘ rangeSplitting F)
⊢ UniformEquicontinuous (ι := { x : β → α // x ∈ range F }) (Subtype.val (p := fun (x : β → α) ↦ x ∈ range F))

Tactic:
rw [← comp_rangeSplitting F]

Premises used: Set.comp_rangeSplitting
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
h : UniformEquicontinuous F
⊢ UniformEquicontinuous (F ∘ rangeSplitting F)

Tactic:
h.comp _

Premises used: UniformEquicontinuous.comp
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
h : UniformEquicontinuous F
⊢ UniformEquicontinuous (F ∘ rangeSplitting F)

Tactic:
exact h.comp _

Premises used: UniformEquicontinuous.comp