awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw : UniformEquicontinuousOn (F ∘ rangeSplitting F) S
⊢ UniformEquicontinuousOn (ι := { x : β → α // x ∈ range F }) (Subtype.val (p := fun (x : β → α) ↦ x ∈ range F)) S

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 : ι → β → α
S : Set β
h : UniformEquicontinuousOn F S
⊢ UniformEquicontinuousOn (F ∘ rangeSplitting F) S

Tactic:
h.comp _

Premises used: UniformEquicontinuousOn.comp
-- 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
⊢ UniformEquicontinuousOn (F ∘ rangeSplitting F) S

Tactic:
exact h.comp _

Premises used: UniformEquicontinuousOn.comp
-- 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
rw :
  EquicontinuousAt F x₀ ↔
    ∀ i ∈ 𝓤 α,
      ∀ᶠ (x : X) in 𝓝 x₀,
        Membership.mem (γ := Set (ι →ᵤ α))
          {g : ι →ᵤ α |
            (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x₀, g) ∈ UniformFun.gen ι α i}
          (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x)
⊢ EquicontinuousAt F x₀ ↔
    ContinuousAt (Y := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x₀

Tactic:
rw [ContinuousAt, (UniformFun.hasBasis_nhds ι α _).tendsto_right_iff]

Premises used: ContinuousAt, Filter.HasBasis.tendsto_right_iff, UniformFun.hasBasis_nhds
-- 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₀ ↔
    ∀ i ∈ 𝓤 α,
      ∀ᶠ (x : X) in 𝓝 x₀,
        Membership.mem (γ := Set (ι →ᵤ α))
          {g : ι →ᵤ α |
            (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x₀, g) ∈ UniformFun.gen ι α i}
          (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x)

Tactic:
rfl
-- 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
rw :
  EquicontinuousWithinAt F S x₀ ↔
    ∀ i ∈ 𝓤 α,
      ∀ᶠ (x : X) in 𝓝[S] x₀,
        Membership.mem (γ := Set (ι →ᵤ α))
          {g : ι →ᵤ α |
            (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x₀, g) ∈ UniformFun.gen ι α i}
          (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x)
⊢ EquicontinuousWithinAt F S x₀ ↔
    ContinuousWithinAt (Y := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) S x₀

Tactic:
rw [ContinuousWithinAt, (UniformFun.hasBasis_nhds ι α _).tendsto_right_iff]

Premises used: ContinuousWithinAt, Filter.HasBasis.tendsto_right_iff, UniformFun.hasBasis_nhds
-- 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₀ ↔
    ∀ i ∈ 𝓤 α,
      ∀ᶠ (x : X) in 𝓝[S] x₀,
        Membership.mem (γ := Set (ι →ᵤ α))
          {g : ι →ᵤ α |
            (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x₀, g) ∈ UniformFun.gen ι α i}
          (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x)

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
simp_rw :
  (∀ (x₀ : X), EquicontinuousAt F x₀) ↔
    Continuous[tX, topologicalSpace ι α] ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F)
simp_rw₁ :
  (∀ (x₀ : X), EquicontinuousAt F x₀) ↔
    ∀ (x : X), ContinuousAt (Y := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x
⊢ Equicontinuous F ↔
    Continuous[tX, topologicalSpace ι α] ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F)

Tactic:
simp_rw [Equicontinuous, continuous_iff_continuousAt, equicontinuousAt_iff_continuousAt]

Premises used: Equicontinuous, equicontinuousAt_iff_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
simp_rw :
  (∀ x₀ ∈ S, EquicontinuousWithinAt F S x₀) ↔
    ContinuousOn (Y := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) S
simp_rw₁ :
  (∀ x₀ ∈ S, EquicontinuousWithinAt F S x₀) ↔
    ∀ x ∈ S,
      ContinuousWithinAt (Y := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) S x
⊢ EquicontinuousOn F S ↔
    ContinuousOn (Y := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) S

Tactic:
simp_rw [EquicontinuousOn, ContinuousOn, equicontinuousWithinAt_iff_continuousWithinAt]

Premises used: equicontinuousWithinAt_iff_continuousWithinAt, EquicontinuousOn, ContinuousOn
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
rw :
  UniformEquicontinuous F ↔
    ∀ 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 ι α i
⊢ UniformEquicontinuous F ↔
    UniformContinuous (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F)

Tactic:
rw [UniformContinuous, (UniformFun.hasBasis_uniformity ι α).tendsto_right_iff]

Premises used: UniformContinuous, UniformFun.hasBasis_uniformity, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
⊢ UniformEquicontinuous F ↔
    ∀ 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 ι α i

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
rw :
  UniformEquicontinuousOn F S ↔
    ∀ i ∈ 𝓤 α,
      ∀ᶠ (x : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S),
        (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F) x.1,
            ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F) x.2) ∈
          UniformFun.gen ι α i
⊢ UniformEquicontinuousOn F S ↔
    UniformContinuousOn (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F) S

Tactic:
rw [UniformContinuousOn, (UniformFun.hasBasis_uniformity ι α).tendsto_right_iff]

Premises used: UniformFun.hasBasis_uniformity, UniformContinuousOn, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
⊢ UniformEquicontinuousOn F S ↔
    ∀ i ∈ 𝓤 α,
      ∀ᶠ (x : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S),
        (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F) x.1,
            ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F) x.2) ∈
          UniformFun.gen ι α i

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
S : Set X
x₀ : X
simp :
  ContinuousWithinAt (Y := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) S
      x₀ ↔
    ∀ (k : κ),
      ContinuousWithinAt (Y := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) S
        x₀
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ (k : κ), EquicontinuousWithinAt F S x₀

Tactic:
simp +instances only [equicontinuousWithinAt_iff_continuousWithinAt (uα := _), topologicalSpace]

Premises used: equicontinuousWithinAt_iff_continuousWithinAt, UniformFun.topologicalSpace
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
S : Set X
x₀ : X
rw :
  Tendsto (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) (𝓝[S] x₀)
      (𝓝 (((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) x₀)) ↔
    ∀ (k : κ),
      Tendsto (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) (𝓝[S] x₀)
        (𝓝 (((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) x₀))
rw₁ :
  Tendsto (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) (𝓝[S] x₀)
      (𝓝 (((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) x₀)) ↔
    ∀ (k : κ),
      Tendsto (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) (𝓝[S] x₀)
        (𝓝 (((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) x₀))
rw₂ :
  Tendsto (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) (𝓝[S] x₀)
      (⨅ (i : κ), 𝓝 (((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) x₀)) ↔
    ∀ (k : κ),
      Tendsto (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) (𝓝[S] x₀)
        (𝓝 (((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) x₀))
rw₃ rw₄ :
  (∀ (i : κ),
      Tendsto (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) (𝓝[S] x₀)
        (𝓝 (((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) x₀))) ↔
    ∀ (k : κ),
      Tendsto (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) (𝓝[S] x₀)
        (𝓝 (((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) x₀))
⊢ Tendsto (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) (𝓝[S] x₀)
      (𝓝 (((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) x₀)) ↔
    ∀ (k : κ),
      Tendsto (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) (𝓝[S] x₀)
        (𝓝 (((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) x₀))

Tactic:
rw [UniformFun.iInf_eq, toTopologicalSpace_iInf, nhds_iInf, tendsto_iInf]

Premises used: nhds_iInf, UniformSpace.toTopologicalSpace_iInf, Filter.tendsto_iInf, UniformFun.iInf_eq
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
x₀ : X
⊢ EquicontinuousAt F x₀ ↔ ∀ (k : κ), EquicontinuousAt F x₀

Tactic:
simp only [← equicontinuousWithinAt_univ (uα := _), equicontinuousWithinAt_iInf_rng]

Premises used: equicontinuousWithinAt_univ, equicontinuousWithinAt_iInf_rng
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
simp_rw :
  Continuous[tX, inferInstance] ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) ↔
    ∀ (k : κ),
      Continuous[tX, inferInstance] ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F)
⊢ Equicontinuous F ↔ ∀ (k : κ), Equicontinuous F

Tactic:
simp_rw +instances [equicontinuous_iff_continuous (uα := _), UniformFun.topologicalSpace]

Premises used: equicontinuous_iff_continuous, UniformFun.topologicalSpace
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
rw :
  Continuous[tX, inferInstance] ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) ↔
    ∀ (k : κ),
      Continuous[tX, inferInstance] ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F)
rw₁ :
  Continuous[tX, inferInstance] ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) ↔
    ∀ (k : κ),
      Continuous[tX, inferInstance] ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F)
rw₂ rw₃ :
  (∀ (i : κ),
      Continuous[tX, (uniformSpace ι α').toTopologicalSpace]
        ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F)) ↔
    ∀ (k : κ),
      Continuous[tX, inferInstance] ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F)
⊢ Continuous[tX, inferInstance] ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F) ↔
    ∀ (k : κ),
      Continuous[tX, inferInstance] ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α') F)

Tactic:
rw [UniformFun.iInf_eq, toTopologicalSpace_iInf, continuous_iInf_rng]

Premises used: continuous_iInf_rng, UniformSpace.toTopologicalSpace_iInf, UniformFun.iInf_eq
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
S : Set X
simp_rw : (∀ x₀ ∈ S, EquicontinuousWithinAt F S x₀) ↔ ∀ (k : κ), ∀ x₀ ∈ S, EquicontinuousWithinAt F S x₀
simp_rw₁ : (∀ x₀ ∈ S, ∀ (k : κ), EquicontinuousWithinAt F S x₀) ↔ ∀ (k : κ), ∀ x₀ ∈ S, EquicontinuousWithinAt F S x₀
⊢ EquicontinuousOn F S ↔ ∀ (k : κ), EquicontinuousOn F S

Tactic:
simp_rw [EquicontinuousOn, equicontinuousWithinAt_iInf_rng, @forall_comm _ κ]

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

Tactic:
simp_rw [uniformEquicontinuous_iff_uniformContinuous (uα := _)]

Premises used: uniformEquicontinuous_iff_uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
rw :
  UniformContinuous (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α') F) ↔
    ∀ (k : κ),
      UniformContinuous (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α') F)
rw₁ rw₂ :
  (∀ (i : κ),
      UniformContinuous (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α') F)) ↔
    ∀ (k : κ),
      UniformContinuous (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α') F)
⊢ UniformContinuous (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α') F) ↔
    ∀ (k : κ),
      UniformContinuous (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α') F)

Tactic:
rw [UniformFun.iInf_eq, uniformContinuous_iInf_rng]

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

Tactic:
simp_rw [uniformEquicontinuousOn_iff_uniformContinuousOn (uα := _)]

Premises used: uniformEquicontinuousOn_iff_uniformContinuousOn
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
S : Set β
rw :
  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)) (𝓤 (ι →ᵤ α')) ↔
    ∀ (k : κ),
      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)) (𝓤 (ι →ᵤ α'))
rw₁ :
  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)) (⨅ (i : κ), 𝓤 (ι →ᵤ α')) ↔
    ∀ (k : κ),
      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)) (𝓤 (ι →ᵤ α'))
rw₂ rw₃ :
  (∀ (i : κ),
      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)) (𝓤 (ι →ᵤ α'))) ↔
    ∀ (k : κ),
      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)) (𝓤 (ι →ᵤ α'))
⊢ 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)) (𝓤 (ι →ᵤ α')) ↔
    ∀ (k : κ),
      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 [UniformFun.iInf_eq, iInf_uniformity, tendsto_iInf]

Premises used: iInf_uniformity, Filter.tendsto_iInf, UniformFun.iInf_eq
-- 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'
x₀ : X'
k : κ
hk : EquicontinuousWithinAt F S x₀
simp :
  ∀
    (hk :
      ContinuousWithinAt (Y := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F) S
        x₀),
    ContinuousWithinAt (Y := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F) S x₀
⊢ EquicontinuousWithinAt F S x₀

Tactic:
simp only [equicontinuousWithinAt_iff_continuousWithinAt (tX := _)] at hk ⊢

Premises used: equicontinuousWithinAt_iff_continuousWithinAt
-- 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'
x₀ : X'
k : κ
hk :
  Tendsto (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F) (𝓝 x₀ ⊓ 𝓟 S)
    (𝓝 (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F) x₀))
rw :
  Tendsto (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F)
    ((⨅ (i : κ), 𝓝 x₀) ⊓ 𝓟 S) (𝓝 (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F) x₀))
⊢ Tendsto (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F) (𝓝 x₀ ⊓ 𝓟 S)
    (𝓝 (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F) x₀))

Tactic:
rw [nhds_iInf]

Premises used: nhds_iInf
-- 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'
x₀ : X'
k : κ
hk :
  Tendsto (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F) (𝓝 x₀ ⊓ 𝓟 S)
    (𝓝 (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F) x₀))
⊢ Tendsto (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F)
    ((⨅ (i : κ), 𝓝 x₀) ⊓ 𝓟 S) (𝓝 (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F) x₀))

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
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
S : Set X'
x₀ : X'
k : κ
hk :
  Tendsto (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F) (𝓝 x₀ ⊓ 𝓟 S)
    (𝓝 (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F) x₀))
⊢ Tendsto (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F)
    ((⨅ (i : κ), 𝓝 x₀) ⊓ 𝓟 S) (𝓝 (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F) x₀))

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_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
x₀ : X'
k : κ
hk : EquicontinuousAt F x₀
rw : ∀ (hk : EquicontinuousWithinAt F univ x₀), EquicontinuousWithinAt F univ x₀
⊢ EquicontinuousAt F x₀

Tactic:
rw [← equicontinuousWithinAt_univ (tX := _)] at hk ⊢

Premises used: equicontinuousWithinAt_univ
-- 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' → α
x₀ : X'
k : κ
hk : EquicontinuousWithinAt F univ x₀
⊢ EquicontinuousWithinAt F univ x₀

Tactic:
equicontinuousWithinAt_iInf_dom hk

Premises used: equicontinuousWithinAt_iInf_dom
-- 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' → α
x₀ : X'
k : κ
hk : EquicontinuousWithinAt F univ x₀
⊢ EquicontinuousWithinAt F univ x₀

Tactic:
exact equicontinuousWithinAt_iInf_dom hk

Premises used: equicontinuousWithinAt_iInf_dom
-- 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' → α
k : κ
hk : Equicontinuous F
⊢ Equicontinuous F

Tactic:
fun x ↦ equicontinuousAt_iInf_dom (hk x)

Premises used: Equicontinuous, equicontinuousAt_iInf_dom