awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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))
    (𝓤 β' ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α))
have 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)) (𝓤 (ι →ᵤ α))
Tactic: rw [iInf_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
⊢ EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U
have 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
Tactic: rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
    hX.tendsto_iff (UniformFun.hasBasis_nhds ι α _)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U
have 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
Tactic: rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt,
    hX.tendsto_iff (UniformFun.hasBasis_nhds ι α _)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
⊢ EquicontinuousAt F x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
have 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
Tactic: rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
    (UniformFun.hasBasis_nhds_of_basis ι α _ hα).tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
have 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
Tactic: rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt,
    (UniformFun.hasBasis_nhds_of_basis ι α _ hα).tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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₂
⊢ EquicontinuousAt F x₀ ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
have 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₂
Tactic: rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
    hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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₂
⊢ EquicontinuousWithinAt F S x₀ ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
have 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₂
Tactic: rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt,
    hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
⊢ UniformEquicontinuous F ↔ ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
have 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
Tactic: rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
    hβ.tendsto_iff (UniformFun.hasBasis_uniformity ι α)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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 ∧
          ∀ 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
have 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
Tactic: simp only [Prod.forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
⊢ UniformEquicontinuousOn F S ↔ ∀ U ∈ 𝓤 α, ∃ (k : κ), p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
have 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
Tactic: rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
    hβ.tendsto_iff (UniformFun.hasBasis_uniformity ι α)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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 ∧
          ∀ 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
have 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
Tactic: simp only [Prod.forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
⊢ UniformEquicontinuous F ↔ ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k
have 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
Tactic: rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
    (UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
⊢ UniformEquicontinuousOn F S ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k
have 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
Tactic: rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
    (UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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₂
⊢ UniformEquicontinuous F ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
have 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₂
Tactic: rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
    hβ.tendsto_iff (UniformFun.hasBasis_uniformity_of_basis ι α hα)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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 ∧
            ∀ 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₂
have 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₂
Tactic: simp only [Prod.forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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₂
⊢ UniformEquicontinuousOn F S ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ (k₁ : κ₁), p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
have 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₂
Tactic: rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
    hβ.tendsto_iff (UniformFun.hasBasis_uniformity_of_basis ι α hα)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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 ∧
            ∀ 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₂
have 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₂
Tactic: simp only [Prod.forall]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (hypothesis)
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
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) x₀
have this : IsInducing (X := ι →ᵤ α) (Y := ι →ᵤ β)
  (Function.comp (β := ι → β) (⇑ofFun : (a : ι → β) → ι →ᵤ β)
    ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
Tactic: have := (UniformFun.postcomp_isUniformInducing (α := ι) hu).isInducing
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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 : ι →ᵤ α) → ι → α)))
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) x₀
have 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₀
Tactic: rw [equicontinuousAt_iff_continuousAt, equicontinuousAt_iff_continuousAt, this.continuousAt_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (hypothesis)
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
⊢ EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) S x₀
have this : IsInducing (X := ι →ᵤ α) (Y := ι →ᵤ β)
  (Function.comp (β := ι → β) (⇑ofFun : (a : ι → β) → ι →ᵤ β)
    ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
Tactic: have := (UniformFun.postcomp_isUniformInducing (α := ι) hu).isInducing
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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 : ι →ᵤ α) → ι → α)))
⊢ EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) S x₀
have 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₀
Tactic: simp only [equicontinuousWithinAt_iff_continuousWithinAt, this.continuousWithinAt_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
⊢ Equicontinuous F ↔ Equicontinuous.{u_1, u_3, u_8} (X := X) (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F)
have a : ∀ (x : X), EquicontinuousAt F x ↔ EquicontinuousAt.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) x
Tactic: congrm ∀ x, ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
⊢ EquicontinuousAt F x ↔ EquicontinuousAt.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) x
have 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
Tactic: rw [hu.equicontinuousAt_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
⊢ EquicontinuousOn F S ↔ EquicontinuousOn.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) S
have a : ∀ (x : X),
  EquicontinuousWithinAt F S x ↔ EquicontinuousWithinAt.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) S x
Tactic: congrm ∀ x ∈ S, ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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
⊢ EquicontinuousWithinAt F S x ↔ EquicontinuousWithinAt.{u_1, u_3, u_8} (α := β) ((fun (x : X → α) ↦ u ∘ x) ∘ F) S x
have 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
Tactic: rw [hu.equicontinuousWithinAt_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (hypothesis)
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : IsUniformInducing u
⊢ UniformEquicontinuous F ↔ UniformEquicontinuous.{u_1, u_10, u_8} (α := γ) (β := β) ((fun (x : β → α) ↦ u ∘ x) ∘ F)
have this : IsUniformInducing (α := ι →ᵤ α) (β := ι →ᵤ γ)
  (Function.comp (β := ι → γ) (⇑ofFun : (a : ι → γ) → ι →ᵤ γ)
    ((fun (x : ι → α) ↦ u ∘ x) ∘ (⇑toFun : (a : ι →ᵤ α) → ι → α)))
Tactic: have := UniformFun.postcomp_isUniformInducing (α := ι) hu