awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
S : Set X'
k : κ
hk : EquicontinuousOn F S
⊢ EquicontinuousOn F S

Tactic:
fun x hx ↦ equicontinuousWithinAt_iInf_dom (hk x hx)

Premises used: equicontinuousWithinAt_iInf_dom, EquicontinuousOn
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
k : κ
hk : UniformEquicontinuous F
simp_rw :
  ∀ (hk : UniformContinuous (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F)),
    UniformContinuous (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F)
⊢ UniformEquicontinuous F

Tactic:
simp_rw [uniformEquicontinuous_iff_uniformContinuous (uβ := _)] at hk ⊢

Premises used: uniformEquicontinuous_iff_uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
k : κ
hk : UniformContinuous (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F)
⊢ UniformContinuous (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F)

Tactic:
uniformContinuous_iInf_dom hk

Premises used: uniformContinuous_iInf_dom
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
k : κ
hk : UniformContinuous (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F)
⊢ UniformContinuous (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F)

Tactic:
exact uniformContinuous_iInf_dom hk

Premises used: uniformContinuous_iInf_dom
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
S : Set β'
k : κ
hk : UniformEquicontinuousOn F S
simp_rw :
  ∀
    (hk :
      UniformContinuousOn (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F) S),
    UniformContinuousOn (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F) S
⊢ UniformEquicontinuousOn F S

Tactic:
simp_rw [uniformEquicontinuousOn_iff_uniformContinuousOn (uβ := _)] at hk ⊢

Premises used: uniformEquicontinuousOn_iff_uniformContinuousOn
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
S : Set β'
k : κ
hk : UniformContinuousOn (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F) S
rw :
  Tendsto (β := (ι →ᵤ α) × (ι →ᵤ α))
    (fun (x : β' × β') ↦
      (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F) x.1,
        ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F) x.2))
    ((⨅ (i : κ), 𝓤 β') ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α))
⊢ Tendsto (β := (ι →ᵤ α) × (ι →ᵤ α))
    (fun (x : β' × β') ↦
      (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F) x.1,
        ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F) x.2))
    (𝓤 β' ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α))

Tactic:
rw [iInf_uniformity]

Premises used: iInf_uniformity
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
S : Set β'
k : κ
hk : UniformContinuousOn (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F) S
⊢ Tendsto (β := (ι →ᵤ α) × (ι →ᵤ α))
    (fun (x : β' × β') ↦
      (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F) x.1,
        ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F) x.2))
    ((⨅ (i : κ), 𝓤 β') ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α))

Tactic:
hk.mono_left <| inf_le_inf_right _ <| iInf_le _ k

Premises used: inf_le_inf_right, Filter.Tendsto.mono_left, iInf_le
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_6
β' : Type u_9
uα : UniformSpace α
u : κ → UniformSpace β'
F : ι → β' → α
S : Set β'
k : κ
hk : UniformContinuousOn (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F) S
⊢ Tendsto (β := (ι →ᵤ α) × (ι →ᵤ α))
    (fun (x : β' × β') ↦
      (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F) x.1,
        ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F) x.2))
    ((⨅ (i : κ), 𝓤 β') ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α))

Tactic:
exact hk.mono_left <| inf_le_inf_right _ <| iInf_le _ k

Premises used: inf_le_inf_right, Filter.Tendsto.mono_left, iInf_le
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set X
F : ι → X → α
x₀ : X
hX : (𝓝 x₀).HasBasis p s
rw :
  (∀ ib ∈ 𝓤 α,
      ∃ (ia : κ),
        p ia ∧
          ∀ x ∈ s ia,
            Membership.mem (γ := Set (ι →ᵤ α))
              {g : ι →ᵤ α |
                (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x₀, g) ∈
                  UniformFun.gen ι α ib}
              (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x)) ↔
    ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U
⊢ EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U

Tactic:
rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
    hX.tendsto_iff (UniformFun.hasBasis_nhds ι α _)]

Premises used: Filter.HasBasis.tendsto_iff, ContinuousAt, equicontinuousAt_iff_continuousAt, UniformFun.hasBasis_nhds
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set X
F : ι → X → α
x₀ : X
hX : (𝓝 x₀).HasBasis p s
⊢ (∀ ib ∈ 𝓤 α,
      ∃ (ia : κ),
        p ia ∧
          ∀ x ∈ s ia,
            Membership.mem (γ := Set (ι →ᵤ α))
              {g : ι →ᵤ α |
                (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x₀, g) ∈
                  UniformFun.gen ι α ib}
              (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x)) ↔
    ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set X
F : ι → X → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p s
rw :
  (∀ ib ∈ 𝓤 α,
      ∃ (ia : κ),
        p ia ∧
          ∀ x ∈ s ia,
            Membership.mem (γ := Set (ι →ᵤ α))
              {g : ι →ᵤ α |
                (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x₀, g) ∈
                  UniformFun.gen ι α ib}
              (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x)) ↔
    ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U

Tactic:
rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt,
    hX.tendsto_iff (UniformFun.hasBasis_nhds ι α _)]

Premises used: ContinuousWithinAt, Filter.HasBasis.tendsto_iff, equicontinuousWithinAt_iff_continuousWithinAt, UniformFun.hasBasis_nhds
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set X
F : ι → X → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p s
⊢ (∀ ib ∈ 𝓤 α,
      ∃ (ia : κ),
        p ia ∧
          ∀ x ∈ s ia,
            Membership.mem (γ := Set (ι →ᵤ α))
              {g : ι →ᵤ α |
                (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x₀, g) ∈
                  UniformFun.gen ι α ib}
              (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x)) ↔
    ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
x₀ : X
hα : (𝓤 α).HasBasis p s
rw :
  (∀ (i : κ),
      p i →
        ∀ᶠ (x : X) in 𝓝 x₀,
          Membership.mem (γ := Set (ι →ᵤ α))
            {g : ι →ᵤ α |
              (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x₀, g) ∈
                UniformFun.gen ι α (s i)}
            (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x)) ↔
    ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
⊢ EquicontinuousAt F x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k

Tactic:
rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
    (UniformFun.hasBasis_nhds_of_basis ι α _ hα).tendsto_right_iff]

Premises used: ContinuousAt, equicontinuousAt_iff_continuousAt, Filter.HasBasis.tendsto_right_iff, UniformFun.hasBasis_nhds_of_basis
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
x₀ : X
hα : (𝓤 α).HasBasis p s
⊢ (∀ (i : κ),
      p i →
        ∀ᶠ (x : X) in 𝓝 x₀,
          Membership.mem (γ := Set (ι →ᵤ α))
            {g : ι →ᵤ α |
              (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x₀, g) ∈
                UniformFun.gen ι α (s i)}
            (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x)) ↔
    ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
S : Set X
x₀ : X
hα : (𝓤 α).HasBasis p s
rw :
  (∀ (i : κ),
      p i →
        ∀ᶠ (x : X) in 𝓝[S] x₀,
          Membership.mem (γ := Set (ι →ᵤ α))
            {g : ι →ᵤ α |
              (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x₀, g) ∈
                UniformFun.gen ι α (s i)}
            (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x)) ↔
    ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k

Tactic:
rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt,
    (UniformFun.hasBasis_nhds_of_basis ι α _ hα).tendsto_right_iff]

Premises used: ContinuousWithinAt, equicontinuousWithinAt_iff_continuousWithinAt, Filter.HasBasis.tendsto_right_iff, UniformFun.hasBasis_nhds_of_basis
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
S : Set X
x₀ : X
hα : (𝓤 α).HasBasis p s
⊢ (∀ (i : κ),
      p i →
        ∀ᶠ (x : X) in 𝓝[S] x₀,
          Membership.mem (γ := Set (ι →ᵤ α))
            {g : ι →ᵤ α |
              (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x₀, g) ∈
                UniformFun.gen ι α (s i)}
            (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x)) ↔
    ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
x₀ : X
hX : (𝓝 x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
rw :
  (∀ (ib : κ₂),
      p₂ ib →
        ∃ (ia : κ₁),
          p₁ ia ∧
            ∀ x ∈ s₁ ia,
              Membership.mem (γ := Set (ι →ᵤ α))
                {g : ι →ᵤ α |
                  (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x₀, g) ∈
                    UniformFun.gen ι α (s₂ ib)}
                (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x)) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
⊢ EquicontinuousAt F x₀ ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂

Tactic:
rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
    hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)]

Premises used: Filter.HasBasis.tendsto_iff, ContinuousAt, equicontinuousAt_iff_continuousAt, UniformFun.hasBasis_nhds_of_basis
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
x₀ : X
hX : (𝓝 x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ (ia : κ₁),
          p₁ ia ∧
            ∀ x ∈ s₁ ia,
              Membership.mem (γ := Set (ι →ᵤ α))
                {g : ι →ᵤ α |
                  (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x₀, g) ∈
                    UniformFun.gen ι α (s₂ ib)}
                (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x)) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
rw :
  (∀ (ib : κ₂),
      p₂ ib →
        ∃ (ia : κ₁),
          p₁ ia ∧
            ∀ x ∈ s₁ ia,
              Membership.mem (γ := Set (ι →ᵤ α))
                {g : ι →ᵤ α |
                  (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x₀, g) ∈
                    UniformFun.gen ι α (s₂ ib)}
                (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x)) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
⊢ EquicontinuousWithinAt F S x₀ ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂

Tactic:
rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt,
    hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)]

Premises used: ContinuousWithinAt, Filter.HasBasis.tendsto_iff, equicontinuousWithinAt_iff_continuousWithinAt, UniformFun.hasBasis_nhds_of_basis
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
S : Set X
x₀ : X
hX : (𝓝[S] x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ (ia : κ₁),
          p₁ ia ∧
            ∀ x ∈ s₁ ia,
              Membership.mem (γ := Set (ι →ᵤ α))
                {g : ι →ᵤ α |
                  (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x₀, g) ∈
                    UniformFun.gen ι α (s₂ ib)}
                (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x)) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
hβ : (𝓤 β).HasBasis p s
rw :
  (∀ ib ∈ 𝓤 α,
      ∃ (ia : κ),
        p ia ∧
          ∀ x ∈ s ia,
            (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F) x.1,
                ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F) x.2) ∈
              UniformFun.gen ι α ib) ↔
    ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
⊢ UniformEquicontinuous F ↔ ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
    hβ.tendsto_iff (UniformFun.hasBasis_uniformity ι α)]

Premises used: UniformContinuous, Filter.HasBasis.tendsto_iff, UniformFun.hasBasis_uniformity, uniformEquicontinuous_iff_uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
hβ : (𝓤 β).HasBasis p s
simp :
  (∀ ib ∈ 𝓤 α,
      ∃ (ia : κ),
        p ia ∧
          ∀ (a b : β),
            (a, b) ∈ s ia →
              (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_2 : β) ↦ α) F) a,
                  ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_2 : β) ↦ α) F) b) ∈
                UniformFun.gen ι α ib) ↔
    ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
⊢ (∀ ib ∈ 𝓤 α,
      ∃ (ia : κ),
        p ia ∧
          ∀ x ∈ s ia,
            (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F) x.1,
                ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F) x.2) ∈
              UniformFun.gen ι α ib) ↔
    ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
simp only [Prod.forall]

Premises used: Prod.forall
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
hβ : (𝓤 β).HasBasis p s
⊢ (∀ ib ∈ 𝓤 α,
      ∃ (ia : κ),
        p ia ∧
          ∀ (a b : β),
            (a, b) ∈ s ia →
              (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_2 : β) ↦ α) F) a,
                  ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_2 : β) ↦ α) F) b) ∈
                UniformFun.gen ι α ib) ↔
    ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s
rw :
  (∀ ib ∈ 𝓤 α,
      ∃ (ia : κ),
        p ia ∧
          ∀ x ∈ s ia,
            (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F) x.1,
                ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F) x.2) ∈
              UniformFun.gen ι α ib) ↔
    ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
⊢ UniformEquicontinuousOn F S ↔ ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
    hβ.tendsto_iff (UniformFun.hasBasis_uniformity ι α)]

Premises used: Filter.HasBasis.tendsto_iff, UniformFun.hasBasis_uniformity, uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s
simp :
  (∀ ib ∈ 𝓤 α,
      ∃ (ia : κ),
        p ia ∧
          ∀ (a b : β),
            (a, b) ∈ s ia →
              (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_2 : β) ↦ α) F) a,
                  ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_2 : β) ↦ α) F) b) ∈
                UniformFun.gen ι α ib) ↔
    ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
⊢ (∀ ib ∈ 𝓤 α,
      ∃ (ia : κ),
        p ia ∧
          ∀ x ∈ s ia,
            (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F) x.1,
                ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F) x.2) ∈
              UniformFun.gen ι α ib) ↔
    ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
simp only [Prod.forall]

Premises used: Prod.forall
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s
⊢ (∀ ib ∈ 𝓤 α,
      ∃ (ia : κ),
        p ia ∧
          ∀ (a b : β),
            (a, b) ∈ s ia →
              (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_2 : β) ↦ α) F) a,
                  ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_2 : β) ↦ α) F) b) ∈
                UniformFun.gen ι α ib) ↔
    ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
hα : (𝓤 α).HasBasis p s
rw :
  (∀ (i : κ),
      p i →
        ∀ᶠ (x : β × β) in 𝓤 β,
          (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F) x.1,
              ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F) x.2) ∈
            (UniformFun.gen ι α ∘ s) i) ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k
⊢ UniformEquicontinuous F ↔ ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
    (UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff]

Premises used: UniformContinuous, UniformFun.hasBasis_uniformity_of_basis, Filter.HasBasis.tendsto_right_iff, uniformEquicontinuous_iff_uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
p : κ → Prop
s : κ → Set (α × α)
F : ι → β → α
hα : (𝓤 α).HasBasis p s
⊢ (∀ (i : κ),
      p i →
        ∀ᶠ (x : β × β) in 𝓤 β,
          (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F) x.1,
              ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F) x.2) ∈
            (UniformFun.gen ι α ∘ s) i) ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
rfl