awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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α : (𝓤 α).HasBasis p s
rw :
  (∀ (i : κ),
      p 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 ι α ∘ s) i) ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k
⊢ UniformEquicontinuousOn F S ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
    (UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff]

Premises used: UniformFun.hasBasis_uniformity_of_basis, uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn, Filter.HasBasis.tendsto_right_iff
-- 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α : (𝓤 α).HasBasis p s
⊢ (∀ (i : κ),
      p 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 ι α ∘ s) i) ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : (𝓤 β).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
rw :
  (∀ (ib : κ₂),
      p₂ 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 ι α ∘ s₂) ib) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
⊢ UniformEquicontinuous F ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

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

Premises used: UniformContinuous, Filter.HasBasis.tendsto_iff, UniformFun.hasBasis_uniformity_of_basis, uniformEquicontinuous_iff_uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : (𝓤 β).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
simp :
  (∀ (ib : κ₂),
      p₂ 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 ι α ∘ s₂) ib) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
⊢ (∀ (ib : κ₂),
      p₂ 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 ι α ∘ s₂) ib) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

Tactic:
simp only [Prod.forall]

Premises used: Prod.forall
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : (𝓤 β).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ 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 ι α ∘ s₂) ib) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
rw :
  (∀ (ib : κ₂),
      p₂ 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 ι α ∘ s₂) ib) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
⊢ UniformEquicontinuousOn F S ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

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

Premises used: Filter.HasBasis.tendsto_iff, UniformFun.hasBasis_uniformity_of_basis, uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
simp :
  (∀ (ib : κ₂),
      p₂ 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 ι α ∘ s₂) ib) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
⊢ (∀ (ib : κ₂),
      p₂ 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 ι α ∘ s₂) ib) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

Tactic:
simp only [Prod.forall]

Premises used: Prod.forall
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ 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 ι α ∘ s₂) ib) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
x₀ : X
u : α → β
hu : IsUniformInducing u
⊢ IsInducing (X := ι →ᵤ α) (Y := ι →ᵤ β)
    (Function.comp (β := ι → β) (⇑ofFun : (a : ι → β) → ι →ᵤ β)
      ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))

Tactic:
have := (UniformFun.postcomp_isUniformInducing (α := ι) hu).isInducing
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
x₀ : X
u : α → β
hu : IsUniformInducing u
this :
  IsInducing (X := ι →ᵤ α) (Y := ι →ᵤ β)
    (Function.comp (β := ι → β) (⇑ofFun : (a : ι → β) → ι →ᵤ β)
      ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
rw :
  ContinuousAt (Y := ι →ᵤ β)
      (Function.comp (β := ι →ᵤ α)
        (Function.comp (β := ι → β) (⇑ofFun : (a : ι → β) → ι →ᵤ β)
          ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
        ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F))
      x₀ ↔
    ContinuousAt (Y := ι →ᵤ β)
      (Function.comp (β := ι → β) (⇑ofFun : (a : ι → β) → ι →ᵤ β)
        (swap (φ := fun (a : ι) (a_1 : X) ↦ β) ((fun (x : X → α) ↦ u ∘ x) ∘ F)))
      x₀
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) x₀

Tactic:
rw [equicontinuousAt_iff_continuousAt, equicontinuousAt_iff_continuousAt, this.continuousAt_iff]

Premises used: Topology.IsInducing.continuousAt_iff, equicontinuousAt_iff_continuousAt
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
x₀ : X
u : α → β
hu : IsUniformInducing u
this :
  IsInducing (X := ι →ᵤ α) (Y := ι →ᵤ β)
    (Function.comp (β := ι → β) (⇑ofFun : (a : ι → β) → ι →ᵤ β)
      ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
⊢ ContinuousAt (Y := ι →ᵤ β)
      (Function.comp (β := ι →ᵤ α)
        (Function.comp (β := ι → β) (⇑ofFun : (a : ι → β) → ι →ᵤ β)
          ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
        ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F))
      x₀ ↔
    ContinuousAt (Y := ι →ᵤ β)
      (Function.comp (β := ι → β) (⇑ofFun : (a : ι → β) → ι →ᵤ β)
        (swap (φ := fun (a : ι) (a_1 : X) ↦ β) ((fun (x : X → α) ↦ u ∘ x) ∘ F)))
      x₀

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
x₀ : X
u : α → β
hu : IsUniformInducing u
⊢ IsInducing (X := ι →ᵤ α) (Y := ι →ᵤ β)
    (Function.comp (β := ι → β) (⇑ofFun : (a : ι → β) → ι →ᵤ β)
      ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))

Tactic:
have := (UniformFun.postcomp_isUniformInducing (α := ι) hu).isInducing
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
x₀ : X
u : α → β
hu : IsUniformInducing u
this :
  IsInducing (X := ι →ᵤ α) (Y := ι →ᵤ β)
    (Function.comp (β := ι → β) (⇑ofFun : (a : ι → β) → ι →ᵤ β)
      ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
simp :
  ContinuousWithinAt (Y := ι →ᵤ β)
      (Function.comp (β := ι →ᵤ α)
        (Function.comp (β := ι → β) (⇑ofFun : (a : ι → β) → ι →ᵤ β)
          ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
        ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F))
      S x₀ ↔
    ContinuousWithinAt (Y := ι →ᵤ β)
      (Function.comp (β := ι → β) (⇑ofFun : (a : ι → β) → ι →ᵤ β)
        (swap (φ := fun (a : ι) (a_1 : X) ↦ β) ((fun (x : X → α) ↦ u ∘ x) ∘ F)))
      S x₀
⊢ EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) S x₀

Tactic:
simp only [equicontinuousWithinAt_iff_continuousWithinAt, this.continuousWithinAt_iff]

Premises used: equicontinuousWithinAt_iff_continuousWithinAt, Topology.IsInducing.continuousWithinAt_iff
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
x₀ : X
u : α → β
hu : IsUniformInducing u
this :
  IsInducing (X := ι →ᵤ α) (Y := ι →ᵤ β)
    (Function.comp (β := ι → β) (⇑ofFun : (a : ι → β) → ι →ᵤ β)
      ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
⊢ ContinuousWithinAt (Y := ι →ᵤ β)
      (Function.comp (β := ι →ᵤ α)
        (Function.comp (β := ι → β) (⇑ofFun : (a : ι → β) → ι →ᵤ β)
          ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
        ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F))
      S x₀ ↔
    ContinuousWithinAt (Y := ι →ᵤ β)
      (Function.comp (β := ι → β) (⇑ofFun : (a : ι → β) → ι →ᵤ β)
        (swap (φ := fun (a : ι) (a_1 : X) ↦ β) ((fun (x : X → α) ↦ u ∘ x) ∘ F)))
      S x₀

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
u : α → β
hu : IsUniformInducing u
a : ∀ (x : X), EquicontinuousAt F x ↔ EquicontinuousAt.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) x
⊢ Equicontinuous F ↔ Equicontinuous.{u_1, u_3, u_8} (X := X) (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F)

Tactic:
congrm ∀ x, ?_
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
u : α → β
hu : IsUniformInducing u
x : X
a a₁ :
  EquicontinuousAt.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) x ↔
    EquicontinuousAt.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) x
⊢ EquicontinuousAt F x ↔ EquicontinuousAt.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) x

Tactic:
rw [hu.equicontinuousAt_iff]

Premises used: IsUniformInducing.equicontinuousAt_iff
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
u : α → β
hu : IsUniformInducing u
a :
  ∀ (x : X),
    EquicontinuousWithinAt F S x ↔ EquicontinuousWithinAt.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) S x
⊢ EquicontinuousOn F S ↔ EquicontinuousOn.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) S

Tactic:
congrm ∀ x ∈ S, ?_
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
u : α → β
hu : IsUniformInducing u
x : X
a a₁ :
  EquicontinuousWithinAt.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) S x ↔
    EquicontinuousWithinAt.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) S x
⊢ EquicontinuousWithinAt F S x ↔ EquicontinuousWithinAt.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) S x

Tactic:
rw [hu.equicontinuousWithinAt_iff]

Premises used: IsUniformInducing.equicontinuousWithinAt_iff
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : IsUniformInducing u
⊢ IsUniformInducing (α := ι →ᵤ α) (β := ι →ᵤ γ)
    (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
      ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))

Tactic:
have := UniformFun.postcomp_isUniformInducing (α := ι) hu
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : IsUniformInducing u
this :
  IsUniformInducing (α := ι →ᵤ α) (β := ι →ᵤ γ)
    (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
      ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
simp :
  UniformContinuous (β := ι →ᵤ γ)
      (Function.comp (β := ι →ᵤ α)
        (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
          ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
        ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F)) ↔
    UniformContinuous (α := β) (β := ι →ᵤ γ)
      (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
        (swap (φ := fun (a : ι) (a_1 : β) ↦ γ) ((fun (x : β → α) ↦ u ∘ x) ∘ F)))
⊢ UniformEquicontinuous F ↔ UniformEquicontinuous.{u_1, u_10, u_8} (α := γ) (β := β) ((fun (x : β → α) ↦ u ∘ x) ∘ F)

Tactic:
simp only [uniformEquicontinuous_iff_uniformContinuous, this.uniformContinuous_iff]

Premises used: IsUniformInducing.uniformContinuous_iff, uniformEquicontinuous_iff_uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : IsUniformInducing u
this :
  IsUniformInducing (α := ι →ᵤ α) (β := ι →ᵤ γ)
    (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
      ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
⊢ UniformContinuous (β := ι →ᵤ γ)
      (Function.comp (β := ι →ᵤ α)
        (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
          ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
        ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F)) ↔
    UniformContinuous (α := β) (β := ι →ᵤ γ)
      (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
        (swap (φ := fun (a : ι) (a_1 : β) ↦ γ) ((fun (x : β → α) ↦ u ∘ x) ∘ F)))

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
S : Set β
u : α → γ
hu : IsUniformInducing u
⊢ IsUniformInducing (α := ι →ᵤ α) (β := ι →ᵤ γ)
    (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
      ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))

Tactic:
have := UniformFun.postcomp_isUniformInducing (α := ι) hu
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
S : Set β
u : α → γ
hu : IsUniformInducing u
this :
  IsUniformInducing (α := ι →ᵤ α) (β := ι →ᵤ γ)
    (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
      ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
simp :
  UniformContinuousOn (β := ι →ᵤ γ)
      (Function.comp (β := ι →ᵤ α)
        (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
          ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
        ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F))
      S ↔
    UniformContinuousOn (β := ι →ᵤ γ)
      (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
        (swap (φ := fun (a : ι) (a_1 : β) ↦ γ) ((fun (x : β → α) ↦ u ∘ x) ∘ F)))
      S
⊢ UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn.{u_1, u_10, u_8} (α := γ) ((fun (x : β → α) ↦ u ∘ x) ∘ F) S

Tactic:
simp only [uniformEquicontinuousOn_iff_uniformContinuousOn, this.uniformContinuousOn_iff]

Premises used: IsUniformInducing.uniformContinuousOn_iff, uniformEquicontinuousOn_iff_uniformContinuousOn
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
S : Set β
u : α → γ
hu : IsUniformInducing u
this :
  IsUniformInducing (α := ι →ᵤ α) (β := ι →ᵤ γ)
    (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
      ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
⊢ UniformContinuousOn (β := ι →ᵤ γ)
      (Function.comp (β := ι →ᵤ α)
        (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
          ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
        ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F))
      S ↔
    UniformContinuousOn (β := ι →ᵤ γ)
      (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
        (swap (φ := fun (a : ι) (a_1 : β) ↦ γ) ((fun (x : β → α) ↦ u ∘ x) ∘ F)))
      S

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : X) ↦ α) ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval (β := fun (x : X) ↦ α) x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
rcases :
  ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVclosed : IsClosed[instTopologicalSpaceProd] V) (hVU : V ⊆ U),
    ∀ᶠ (x : X) in 𝓝[S] x₀,
      ∀ (i : (↑(closure[tY] A) : Type u_5)),
        ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i x₀,
            (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i x) ∈
          U
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀,
    ∀ (i : (↑(closure[tY] A) : Type u_5)),
      ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i x₀,
          (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i x) ∈
        U

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

Premises used: mem_uniformity_isClosed
-- Module: Mathlib.Topology.UniformSpace.Equicontinuity
Goal:
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (ι := (↑A : Type u_5)) (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.restrict (π := fun (a : X) ↦ α) ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval (β := fun (x : X) ↦ α) x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
h :
  ∀ (x : X)
    (hx :
      ∀ (i : (↑A : Type u_5)),
        ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) i x₀, (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ A)) i x) ∈ V)
    (hxS : x ∈ S) (i : (↑(closure[tY] A) : Type u_5)),
    ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i x₀,
        (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i x) ∈
      U
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀,
    ∀ (i : (↑(closure[tY] A) : Type u_5)),
      ((u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i x₀,
          (u ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ closure[tY] A)) i x) ∈
        U

Tactic:
filter_upwards [hA V hV, eventually_mem_nhdsWithin] with x hx hxS

Premises used: eventually_mem_nhdsWithin