awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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₀))
⊢ 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₀))
have 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₀))
Tactic: rw [UniformFun.iInf_eq, toTopologicalSpace_iInf, nhds_iInf, tendsto_iInf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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₀))
⊢ 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₀))
have 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₀))
Tactic: rw [UniformFun.iInf_eq, toTopologicalSpace_iInf, nhds_iInf, tendsto_iInf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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₀))
⊢ 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₀))
have 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₀))
Tactic: rw [UniformFun.iInf_eq, toTopologicalSpace_iInf, nhds_iInf, tendsto_iInf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
⊢ Equicontinuous F ↔ ∀ (k : κ), Equicontinuous F
have 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)
Tactic: simp_rw +instances [equicontinuous_iff_continuous (uα := _), UniformFun.topologicalSpace]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
⊢ 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)
have 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)
Tactic: rw [UniformFun.iInf_eq, toTopologicalSpace_iInf, continuous_iInf_rng]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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)
⊢ 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)
have 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)
Tactic: rw [UniformFun.iInf_eq, toTopologicalSpace_iInf, continuous_iInf_rng]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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)
⊢ 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)
have 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)
Tactic: rw [UniformFun.iInf_eq, toTopologicalSpace_iInf, continuous_iInf_rng]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
S : Set X
⊢ EquicontinuousOn F S ↔ ∀ (k : κ), EquicontinuousOn F S
have simp_rw : (∀ x₀ ∈ S, EquicontinuousWithinAt F S x₀) ↔ ∀ (k : κ), ∀ x₀ ∈ S, EquicontinuousWithinAt F S x₀
Tactic: simp_rw [EquicontinuousOn, equicontinuousWithinAt_iInf_rng, @forall_comm _ κ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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₀
⊢ EquicontinuousOn F S ↔ ∀ (k : κ), EquicontinuousOn F S
have simp_rw₁ : (∀ x₀ ∈ S, ∀ (k : κ), EquicontinuousWithinAt F S x₀) ↔ ∀ (k : κ), ∀ x₀ ∈ S, EquicontinuousWithinAt F S x₀
Tactic: simp_rw [EquicontinuousOn, equicontinuousWithinAt_iInf_rng, @forall_comm _ κ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
⊢ UniformEquicontinuous F ↔ ∀ (k : κ), UniformEquicontinuous F
have simp_rw : UniformContinuous (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α') F) ↔
  ∀ (k : κ),
    UniformContinuous (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α') F)
Tactic: simp_rw [uniformEquicontinuous_iff_uniformContinuous (uα := _)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
⊢ UniformContinuous (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α') F) ↔
    ∀ (k : κ),
      UniformContinuous (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α') F)
have rw : 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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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)
⊢ UniformContinuous (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α') F) ↔
    ∀ (k : κ),
      UniformContinuous (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α') F)
have rw₁ : (∀ (i : κ),
    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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
S : Set β
⊢ UniformEquicontinuousOn F S ↔ ∀ (k : κ), UniformEquicontinuousOn F S
have simp_rw : UniformContinuousOn (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α') F) S ↔
  ∀ (k : κ),
    UniformContinuousOn (β := ι →ᵤ α') ((⇑ofFun : (a : ι → α') → ι →ᵤ α') ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α') F) S
Tactic: simp_rw [uniformEquicontinuousOn_iff_uniformContinuousOn (uα := _)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
κ : Type u_2
α' : Type u_7
β : Type u_8
uβ : UniformSpace β
u : κ → UniformSpace α'
F : ι → β → α'
S : Set β
⊢ 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)) (𝓤 (ι →ᵤ α'))
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))
    (𝓤 β ⊓ 𝓟 (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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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)) (𝓤 (ι →ᵤ α'))
⊢ 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)) (𝓤 (ι →ᵤ α'))
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))
    (𝓤 β ⊓ 𝓟 (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)) (𝓤 (ι →ᵤ α'))
Tactic: rw [UniformFun.iInf_eq, iInf_uniformity, tendsto_iInf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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)) (𝓤 (ι →ᵤ α'))
⊢ 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)) (𝓤 (ι →ᵤ α'))
have 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)) (𝓤 (ι →ᵤ α'))
Tactic: rw [UniformFun.iInf_eq, iInf_uniformity, tendsto_iInf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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₀
⊢ EquicontinuousWithinAt F S x₀
have 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₀
Tactic: simp only [equicontinuousWithinAt_iff_continuousWithinAt (tX := _)] at hk ⊢
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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) (𝓝 x₀ ⊓ 𝓟 S)
    (𝓝 (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F) x₀))
have rw : Tendsto (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F)
  ((⨅ (i : κ), 𝓝 x₀) ⊓ 𝓟 S) (𝓝 (((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X') ↦ α) F) x₀))
Tactic: rw [nhds_iInf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
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₀
⊢ EquicontinuousAt F x₀
have rw : ∀ (hk : EquicontinuousWithinAt F univ x₀), EquicontinuousWithinAt F univ x₀
Tactic: rw [← equicontinuousWithinAt_univ (tX := _)] at hk ⊢
Cleared hypotheses: hk
-- 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 : ι → β' → α
k : κ
hk : UniformEquicontinuous F
⊢ UniformEquicontinuous F
have simp_rw : ∀ (hk : UniformContinuous (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F)),
  UniformContinuous (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F)
Tactic: simp_rw [uniformEquicontinuous_iff_uniformContinuous (uβ := _)] at hk ⊢
Cleared hypotheses: hk
-- 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 : UniformEquicontinuousOn F S
⊢ UniformEquicontinuousOn F S
have simp_rw : ∀
  (hk :
    UniformContinuousOn (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F) S),
  UniformContinuousOn (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β') ↦ α) F) S
Tactic: simp_rw [uniformEquicontinuousOn_iff_uniformContinuousOn (uβ := _)] at hk ⊢
Cleared hypotheses: hk