awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.DiscreteUniformity (goal)
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
Y : Type u_2
inst_1 : Finite Y
inst_2 : UniformSpace Y
inst_3 : DiscreteTopology Y
h : Eq.{u_2 + 1} (α := SetRel Y Y) SetRel.id (⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1})
⊢ DiscreteUniformity Y
have simp_rw : SetRel.id ∈ uniformity Y
Tactic: simp_rw [discreteUniformity_iff_setRelId_mem_uniformity, h, Filter.iInter_mem,
    ← mem_nhds_uniformity_iff_left, nhds_discrete, Filter.mem_pure, Set.mem_singleton_iff,
    implies_true]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.DiscreteUniformity (goal)
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
Y : Type u_2
inst_1 : Finite Y
inst_2 : UniformSpace Y
inst_3 : DiscreteTopology Y
h : Eq.{u_2 + 1} (α := SetRel Y Y) SetRel.id (⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1})
simp_rw : SetRel.id ∈ uniformity Y
⊢ DiscreteUniformity Y
have simp_rw₁ : ⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1} ∈ uniformity Y
Tactic: simp_rw [discreteUniformity_iff_setRelId_mem_uniformity, h, Filter.iInter_mem,
    ← mem_nhds_uniformity_iff_left, nhds_discrete, Filter.mem_pure, Set.mem_singleton_iff,
    implies_true]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.DiscreteUniformity (goal)
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
Y : Type u_2
inst_1 : Finite Y
inst_2 : UniformSpace Y
inst_3 : DiscreteTopology Y
h : Eq.{u_2 + 1} (α := SetRel Y Y) SetRel.id (⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1})
simp_rw : SetRel.id ∈ uniformity Y
simp_rw₁ : ⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1} ∈ uniformity Y
⊢ DiscreteUniformity Y
have simp_rw₂ : ∀ (i : Y), {p : Y × Y | p.2 = i → Membership.mem (γ := Set Y) {i} p.1} ∈ uniformity Y
Tactic: simp_rw [discreteUniformity_iff_setRelId_mem_uniformity, h, Filter.iInter_mem,
    ← mem_nhds_uniformity_iff_left, nhds_discrete, Filter.mem_pure, Set.mem_singleton_iff,
    implies_true]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.DiscreteUniformity (goal)
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
Y : Type u_2
inst_1 : Finite Y
inst_2 : UniformSpace Y
inst_3 : DiscreteTopology Y
h : Eq.{u_2 + 1} (α := SetRel Y Y) SetRel.id (⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1})
simp_rw : SetRel.id ∈ uniformity Y
simp_rw₁ : ⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1} ∈ uniformity Y
simp_rw₂ : ∀ (i : Y), {p : Y × Y | p.2 = i → Membership.mem (γ := Set Y) {i} p.1} ∈ uniformity Y
⊢ DiscreteUniformity Y
have simp_rw₃ : ∀ (i : Y), {i} ∈ nhds i
Tactic: simp_rw [discreteUniformity_iff_setRelId_mem_uniformity, h, Filter.iInter_mem,
    ← mem_nhds_uniformity_iff_left, nhds_discrete, Filter.mem_pure, Set.mem_singleton_iff,
    implies_true]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.DiscreteUniformity (goal)
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
Y : Type u_2
inst_1 : Finite Y
inst_2 : UniformSpace Y
inst_3 : DiscreteTopology Y
h : Eq.{u_2 + 1} (α := SetRel Y Y) SetRel.id (⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1})
simp_rw : SetRel.id ∈ uniformity Y
simp_rw₁ : ⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1} ∈ uniformity Y
simp_rw₂ : ∀ (i : Y), {p : Y × Y | p.2 = i → Membership.mem (γ := Set Y) {i} p.1} ∈ uniformity Y
simp_rw₃ : ∀ (i : Y), {i} ∈ nhds i
⊢ DiscreteUniformity Y
have simp_rw₄ : ∀ (i : Y), Membership.mem (γ := Filter Y) (pure i) {i}
Tactic: simp_rw [discreteUniformity_iff_setRelId_mem_uniformity, h, Filter.iInter_mem,
    ← mem_nhds_uniformity_iff_left, nhds_discrete, Filter.mem_pure, Set.mem_singleton_iff,
    implies_true]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.DiscreteUniformity (goal)
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
Y : Type u_2
inst_1 : Finite Y
inst_2 : UniformSpace Y
inst_3 : DiscreteTopology Y
h : Eq.{u_2 + 1} (α := SetRel Y Y) SetRel.id (⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1})
simp_rw : SetRel.id ∈ uniformity Y
simp_rw₁ : ⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1} ∈ uniformity Y
simp_rw₂ : ∀ (i : Y), {p : Y × Y | p.2 = i → Membership.mem (γ := Set Y) {i} p.1} ∈ uniformity Y
simp_rw₃ : ∀ (i : Y), {i} ∈ nhds i
simp_rw₄ : ∀ (i : Y), Membership.mem (γ := Filter Y) (pure i) {i}
⊢ DiscreteUniformity Y
have simp_rw₅ : ∀ (i : Y), Membership.mem (γ := Set Y) {i} i
Tactic: simp_rw [discreteUniformity_iff_setRelId_mem_uniformity, h, Filter.iInter_mem,
    ← mem_nhds_uniformity_iff_left, nhds_discrete, Filter.mem_pure, Set.mem_singleton_iff,
    implies_true]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.DiscreteUniformity (goal)
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
Y : Type u_2
inst_1 : Finite Y
inst_2 : UniformSpace Y
inst_3 : DiscreteTopology Y
h : Eq.{u_2 + 1} (α := SetRel Y Y) SetRel.id (⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1})
simp_rw : SetRel.id ∈ uniformity Y
simp_rw₁ : ⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1} ∈ uniformity Y
simp_rw₂ : ∀ (i : Y), {p : Y × Y | p.2 = i → Membership.mem (γ := Set Y) {i} p.1} ∈ uniformity Y
simp_rw₃ : ∀ (i : Y), {i} ∈ nhds i
simp_rw₄ : ∀ (i : Y), Membership.mem (γ := Filter Y) (pure i) {i}
simp_rw₅ : ∀ (i : Y), Membership.mem (γ := Set Y) {i} i
⊢ DiscreteUniformity Y
have simp_rw₆ : ∀ (i : Y), True
Tactic: simp_rw [discreteUniformity_iff_setRelId_mem_uniformity, h, Filter.iInter_mem,
    ← mem_nhds_uniformity_iff_left, nhds_discrete, Filter.mem_pure, Set.mem_singleton_iff,
    implies_true]
-- 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 α
F : ι → X → α
x₀ : X
⊢ EquicontinuousWithinAt F univ x₀ ↔ EquicontinuousAt F x₀
have rw : (∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[univ] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U) ↔ EquicontinuousAt F x₀
Tactic: rw [EquicontinuousWithinAt, EquicontinuousAt, nhdsWithin_univ]
-- 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 α
F : ι → X → α
x₀ : X
rw : (∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[univ] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U) ↔ EquicontinuousAt F x₀
⊢ EquicontinuousWithinAt F univ x₀ ↔ EquicontinuousAt F x₀
have rw₁ : (∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[univ] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U) ↔
  ∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
Tactic: rw [EquicontinuousWithinAt, EquicontinuousAt, nhdsWithin_univ]
-- 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 α
F : ι → X → α
x₀ : X
rw : (∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[univ] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U) ↔ EquicontinuousAt F x₀
rw₁ :
  (∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[univ] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U) ↔
    ∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
⊢ EquicontinuousWithinAt F univ x₀ ↔ EquicontinuousAt F x₀
have rw₂ : (∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U) ↔
  ∀ U ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
Tactic: rw [EquicontinuousWithinAt, EquicontinuousAt, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
U : Set (α × α)
| 𝓤 β ⊓ 𝓟 (S ×ˢ S)
have rw : map (α := { x : β // x ∈ S } × { x : β // x ∈ S })
  (Prod.map (Subtype.val (p := fun (x : β) ↦ x ∈ S)) (Subtype.val (p := fun (x : β) ↦ x ∈ S)))
  (Filter.comap (Prod.map (Subtype.val (p := fun (x : β) ↦ x ∈ S)) (Subtype.val (p := fun (x : β) ↦ x ∈ S))) (𝓤 β))
Tactic: rw [← Subtype.range_val (s := S), ← range_prodMap, ← map_comap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
⊢ (∀ U ∈ 𝓤 α,
      ∀ᶠ (xy : (↑S : Type u_8) × (↑S : Type u_8)) in 𝓤 (↑S : Type u_8),
        ∀ (i : ι),
          ((S.restrict (π := fun (a : β) ↦ α) ∘ F) i xy.1, (S.restrict (π := fun (a : β) ↦ α) ∘ F) i xy.2) ∈ U) ↔
    ∀ U ∈ 𝓤 α, ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ U
have conv : (∀ U ∈ 𝓤 α,
    ∀ᶠ (xy : (↑S : Type u_8) × (↑S : Type u_8)) in 𝓤 (↑S : Type u_8),
      ∀ (i : ι), ((S.restrict (π := fun (a : β) ↦ α) ∘ F) i xy.1, (S.restrict (π := fun (a : β) ↦ α) ∘ F) i xy.2) ∈ U) ↔
  ∀ U ∈ 𝓤 α,
    ∀ᶠ (xy : β × β) in
      map (α := { x : β // x ∈ S } × { x : β // x ∈ S })
        (Prod.map (Subtype.val (p := fun (x : β) ↦ x ∈ S)) (Subtype.val (p := fun (x : β) ↦ x ∈ S)))
        (Filter.comap (Prod.map (Subtype.val (p := fun (x : β) ↦ x ∈ S)) (Subtype.val (p := fun (x : β) ↦ x ∈ S)))
          (𝓤 β)),
      ∀ (i : ι), (F i xy.1, F i xy.2) ∈ U
Tactic: conv in _ ⊓ _ => rw [← Subtype.range_val (s := S), ← range_prodMap, ← map_comap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst : Finite ι
F : ι → β → α
⊢ UniformEquicontinuous F ↔ ∀ (i : ι), UniformContinuous (F i)
have simp : (∀ (b : ι) (a : Set (α × α)) (a_1 : a ∈ 𝓤 α), ∀ᶠ (x : β × β) in 𝓤 β, (F b x.1, F b x.2) ∈ a) ↔
  ∀ (i : ι), UniformContinuous (F i)
Tactic: simp only [UniformEquicontinuous, eventually_all, @forall_comm _ ι]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst : Finite ι
F : ι → β → α
S : Set β
⊢ UniformEquicontinuousOn F S ↔ ∀ (i : ι), UniformContinuousOn (F i) S
have simp : (∀ (b : ι) (a : Set (α × α)) (a_1 : a ∈ 𝓤 α), ∀ᶠ (x : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), (F b x.1, F b x.2) ∈ a) ↔
  ∀ (i : ι), UniformContinuousOn (F i) S
Tactic: simp only [UniformEquicontinuousOn, eventually_all, @forall_comm _ ι]
-- 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 α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
have mp : EquicontinuousWithinAt F S x₀ → ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
Tactic: constructor
-- 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 α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
mp : EquicontinuousWithinAt F S x₀ → ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
have mpr : (∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U) → EquicontinuousWithinAt F S x₀
Tactic: constructor
-- 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 α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : EquicontinuousWithinAt F S x₀
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
have mp : ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVsymm : SetRel.IsSymm V) (hVU : SetRel.comp V V ⊆ U),
  ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
Tactic: rcases comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVsymm, hVU⟩
-- 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 α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : EquicontinuousWithinAt F S x₀
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
⊢ ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
have mp : ∀ (x : X) (hx : Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ ∀ (i : ι), (F i x₀, F i x) ∈ V) x} x) (y : X)
  (hy : Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ ∀ (i : ι), (F i x₀, F i x) ∈ V) x} y) (i : ι),
  (F i x, F i x₀) ∈ V
Tactic: refine ⟨_, H V hV, fun x hx y hy i => hVU (SetRel.prodMk_mem_comp ?_ (hy i))⟩
-- 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 α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
have mpr : ∀ (V : Set X) (hV : V ∈ 𝓝[S] x₀) (hVU : ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U),
  ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
Tactic: rcases H U hU with ⟨V, hV, hVU⟩
-- 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 α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set X
hV : V ∈ 𝓝[S] x₀
hVU : ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
have h : ∀ (a : X),
  Membership.mem (γ := Set X)
    {x : X | x ∈ V → Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ ∀ (i : ι), (F i x₀, F i x) ∈ U) x} x} a
Tactic: filter_upwards [hV] using fun x hx i => hVU x₀ (mem_of_mem_nhdsWithin hx₀ hV) x hx i
-- 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 α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set X
hV : V ∈ 𝓝[S] x₀
hVU : ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
h :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X | x ∈ V → Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ ∀ (i : ι), (F i x₀, F i x) ∈ U) x} x} a
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
have h₁ : ∀ a ∈ V, ∀ (i : ι), (F i x₀, F i a) ∈ U
Tactic: filter_upwards [hV] using fun x hx i => hVU x₀ (mem_of_mem_nhdsWithin hx₀ hV) x hx i
-- 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 α
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
have simp_rw : EquicontinuousWithinAt F univ x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
Tactic: simp_rw [← equicontinuousWithinAt_univ, equicontinuousWithinAt_iff_pair (mem_univ x₀),
    nhdsWithin_univ]
-- 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 α
F : ι → X → α
x₀ : X
simp_rw : EquicontinuousWithinAt F univ x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
⊢ EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
have simp_rw₁ : (∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[univ] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U) ↔
  ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
Tactic: simp_rw [← equicontinuousWithinAt_univ, equicontinuousWithinAt_iff_pair (mem_univ x₀),
    nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
h : UniformEquicontinuous F
⊢ UniformEquicontinuous (ι := { x : β → α // x ∈ range F }) (Subtype.val (p := fun (x : β → α) ↦ x ∈ range F))
have rw : UniformEquicontinuous (F ∘ rangeSplitting F)
Tactic: rw [← comp_rangeSplitting F]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
h : UniformEquicontinuousOn F S
⊢ UniformEquicontinuousOn (ι := { x : β → α // x ∈ range F }) (Subtype.val (p := fun (x : β → α) ↦ x ∈ range F)) S
have rw : UniformEquicontinuousOn (F ∘ rangeSplitting F) S
Tactic: rw [← comp_rangeSplitting F]
-- 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 α
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔
    ContinuousAt (Y := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x₀
have 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)
Tactic: rw [ContinuousAt, (UniformFun.hasBasis_nhds ι α _).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 α
F : ι → X → α
S : Set X
x₀ : X
⊢ EquicontinuousWithinAt F S x₀ ↔
    ContinuousWithinAt (Y := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) S x₀
have 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)
Tactic: rw [ContinuousWithinAt, (UniformFun.hasBasis_nhds ι α _).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 α
F : ι → X → α
⊢ Equicontinuous F ↔
    Continuous[tX, topologicalSpace ι α] ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F)
have simp_rw : (∀ (x₀ : X), EquicontinuousAt F x₀) ↔
  Continuous[tX, topologicalSpace ι α] ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F)
Tactic: simp_rw [Equicontinuous, continuous_iff_continuousAt, equicontinuousAt_iff_continuousAt]
-- 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 α
F : ι → X → α
simp_rw :
  (∀ (x₀ : X), EquicontinuousAt F x₀) ↔
    Continuous[tX, topologicalSpace ι α] ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F)
⊢ Equicontinuous F ↔
    Continuous[tX, topologicalSpace ι α] ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F)
have simp_rw₁ : (∀ (x₀ : X), EquicontinuousAt F x₀) ↔
  ∀ (x : X), ContinuousAt (Y := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) x
Tactic: simp_rw [Equicontinuous, continuous_iff_continuousAt, equicontinuousAt_iff_continuousAt]
-- 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 α
F : ι → X → α
S : Set X
⊢ EquicontinuousOn F S ↔
    ContinuousOn (Y := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) S
have simp_rw : (∀ x₀ ∈ S, EquicontinuousWithinAt F S x₀) ↔
  ContinuousOn (Y := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) S
Tactic: simp_rw [EquicontinuousOn, ContinuousOn, equicontinuousWithinAt_iff_continuousWithinAt]
-- 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 α
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
⊢ EquicontinuousOn F S ↔
    ContinuousOn (Y := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) S
have simp_rw₁ : (∀ x₀ ∈ S, EquicontinuousWithinAt F S x₀) ↔
  ∀ x ∈ S,
    ContinuousWithinAt (Y := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : X) ↦ α) F) S x
Tactic: simp_rw [EquicontinuousOn, ContinuousOn, equicontinuousWithinAt_iff_continuousWithinAt]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
⊢ UniformEquicontinuous F ↔
    UniformContinuous (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F)
have 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
Tactic: rw [UniformContinuous, (UniformFun.hasBasis_uniformity ι α).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 β
F : ι → β → α
S : Set β
⊢ UniformEquicontinuousOn F S ↔
    UniformContinuousOn (β := ι →ᵤ α) ((⇑ofFun : (a : ι → α) → ι →ᵤ α) ∘ swap (φ := fun (a : ι) (a_1 : β) ↦ α) F) S
have 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
Tactic: rw [UniformContinuousOn, (UniformFun.hasBasis_uniformity ι α).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_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
S : Set X
x₀ : X
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ (k : κ), EquicontinuousWithinAt F S x₀
have 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₀
Tactic: simp +instances only [equicontinuousWithinAt_iff_continuousWithinAt (uα := _), 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 → α'
S : Set X
x₀ : 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]