awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ (n : ι), s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
k l : ι
⊢ ∃ (i' : ι), True ∧ UniformOnFun.gen 𝔖 (t i') (V i') ⊆ UniformOnFun.gen 𝔖 (t (k, l).1) (V (k, l).2)
have refine_1 : ∀ (n : ι) (hkn : k ≤ n) (hln : l ≤ n),
  ∃ (i' : ι), True ∧ UniformOnFun.gen 𝔖 (t i') (V i') ⊆ UniformOnFun.gen 𝔖 (t (k, l).1) (V (k, l).2)
Tactic: rcases directed_of (· ≤ ·) k l with ⟨n, hkn, hln⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ LE.le (α := Filter (UniformFun.{u_1, u_2} (↑s : Type u_1) β × UniformFun.{u_1, u_2} (↑s : Type u_1) β))
    (map
      (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
        (Function.comp (β := (↑s : Type u_1) → β)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
              (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
            (Function.comp (β := (a : α) → β) (s.restrict (π := fun (a : α) ↦ β))
                (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑s : Type u_1) → β)
            x.1,
          Function.comp (β := (↑s : Type u_1) → β)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
              (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
            (Function.comp (β := (a : α) → β) (s.restrict (π := fun (a : α) ↦ β))
                (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑s : Type u_1) → β)
            x.2))
      (𝓤 (α →ᵤ[𝔖] β)))
    (𝓤 (UniformFun.{u_1, u_2} (↑s : Type u_1) β))
have simp : LE.le (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β))
  (comap (β := UniformFun.{u_1, u_2} (↑s : Type u_1) β × UniformFun.{u_1, u_2} (↑s : Type u_1) β)
    (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
      (Function.comp (β := (↑s : Type u_1) → β)
          ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
            (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
          (Function.comp (β := (a : α) → β) (s.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
            (α →ᵤ[𝔖] β) → (↑s : Type u_1) → β)
          x.1,
        Function.comp (β := (↑s : Type u_1) → β)
          ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
            (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
          (Function.comp (β := (a : α) → β) (s.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
            (α →ᵤ[𝔖] β) → (↑s : Type u_1) → β)
          x.2))
    (𝓤 (UniformFun.{u_1, u_2} (↑s : Type u_1) β)))
Tactic: simp only [map_le_iff_le_comap, iInf_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
⊢ IsUniformEmbedding (α := α →ᵤ[{s : Set α | s.Finite}] β) (β := α → β)
    (⇑(toFun {s : Set α | s.Finite}) : (a : α →ᵤ[{s : Set α | s.Finite}] β) → α → β)
have refine : Eq (α := Filter ((α →ᵤ[{s : Set α | s.Finite}] β) × (α →ᵤ[{s : Set α | s.Finite}] β)))
  (comap (β := (α → β) × (α → β))
    (fun (x : (α →ᵤ[{s : Set α | s.Finite}] β) × (α →ᵤ[{s : Set α | s.Finite}] β)) ↦
      ((toFun {s : Set α | s.Finite} : (a : α →ᵤ[{s : Set α | s.Finite}] β) → α → β) x.1,
        (toFun {s : Set α | s.Finite} : (a : α →ᵤ[{s : Set α | s.Finite}] β) → α → β) x.2))
    (𝓤 (α → β)))
  (𝓤 (α →ᵤ[{s : Set α | s.Finite}] β))
Tactic: refine ⟨⟨?_⟩, Function.injective_id⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
⊢ Eq (α := Filter ((α →ᵤ[{s : Set α | s.Finite}] β) × (α →ᵤ[{s : Set α | s.Finite}] β)))
    (comap (β := (α → β) × (α → β))
      (fun (x : (α →ᵤ[{s : Set α | s.Finite}] β) × (α →ᵤ[{s : Set α | s.Finite}] β)) ↦
        ((toFun {s : Set α | s.Finite} : (a : α →ᵤ[{s : Set α | s.Finite}] β) → α → β) x.1,
          (toFun {s : Set α | s.Finite} : (a : α →ᵤ[{s : Set α | s.Finite}] β) → α → β) x.2))
      (𝓤 (α → β)))
    (𝓤 (α →ᵤ[{s : Set α | s.Finite}] β))
have simp_rw : Eq (α := Filter ((α →ᵤ[{s : Set α | s.Finite}] β) × (α →ᵤ[{s : Set α | s.Finite}] β)))
  (⨅ (i : α),
    comap
      ((fun (a : ((i : α) → β) × ((i : α) → β)) ↦ (a.1 i, a.2 i)) ∘
        fun (x : (α →ᵤ[{s : Set α | s.Finite}] β) × (α →ᵤ[{s : Set α | s.Finite}] β)) ↦
        ((toFun {s : Set α | s.Finite} : (a : α →ᵤ[{s : Set α | s.Finite}] β) → α → β) x.1,
          (toFun {s : Set α | s.Finite} : (a : α →ᵤ[{s : Set α | s.Finite}] β) → α → β) x.2))
      (𝓤 β))
  (𝓤 (α →ᵤ[{s : Set α | s.Finite}] β))
Tactic: simp_rw [Pi.uniformity, comap_iInf, comap_comap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
⊢ Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (𝓤 (α →ᵤ[𝔖] β))
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))
have simp_rw : Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β))
  (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))
Tactic: simp_rw [iInf_uniformity, uniformity_comap,
    (UniformFun.hasBasis_uniformity_of_basis _ _ h).eq_biInf, comap_iInf, comap_principal,
    Function.comp_apply, UniformFun.gen, Subtype.forall, UniformOnFun.gen, preimage_setOf_eq,
    Prod.map_fst, Prod.map_snd, Function.comp_apply, UniformFun.toFun_ofFun, restrict_apply]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
simp_rw :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β))
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))
⊢ Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (𝓤 (α →ᵤ[𝔖] β))
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))
have simp_rw₁ : Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
  (⨅ i ∈ 𝔖,
    comap (β := UniformFun.{u_1, u_2} (↑i : Type u_1) β × UniformFun.{u_1, u_2} (↑i : Type u_1) β)
      (Prod.map
        (Function.comp (β := (↑i : Type u_1) → β)
          ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
            (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
          (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
            (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
        (Function.comp (β := (↑i : Type u_1) → β)
          ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
            (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
          (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
            (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β)))
      (𝓤 (UniformFun.{u_1, u_2} (↑i : Type u_1) β)))
  (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))
Tactic: simp_rw [iInf_uniformity, uniformity_comap,
    (UniformFun.hasBasis_uniformity_of_basis _ _ h).eq_biInf, comap_iInf, comap_principal,
    Function.comp_apply, UniformFun.gen, Subtype.forall, UniformOnFun.gen, preimage_setOf_eq,
    Prod.map_fst, Prod.map_snd, Function.comp_apply, UniformFun.toFun_ofFun, restrict_apply]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
simp_rw :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β))
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))
simp_rw₁ :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (⨅ i ∈ 𝔖,
      comap (β := UniformFun.{u_1, u_2} (↑i : Type u_1) β × UniformFun.{u_1, u_2} (↑i : Type u_1) β)
        (Prod.map
          (Function.comp (β := (↑i : Type u_1) → β)
            ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
              (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
            (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
          (Function.comp (β := (↑i : Type u_1) → β)
            ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
              (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
            (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β)))
        (𝓤 (UniformFun.{u_1, u_2} (↑i : Type u_1) β)))
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))
⊢ Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (𝓤 (α →ᵤ[𝔖] β))
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))
have simp_rw₂ : Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
  (⨅ i ∈ 𝔖,
    comap (β := UniformFun.{u_1, u_2} (↑i : Type u_1) β × UniformFun.{u_1, u_2} (↑i : Type u_1) β)
      (Prod.map
        (Function.comp (β := (↑i : Type u_1) → β)
          ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
            (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
          (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
            (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
        (Function.comp (β := (↑i : Type u_1) → β)
          ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
            (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
          (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
            (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β)))
      (⨅ (i_1 : ι), ⨅ (_ : p i_1), 𝓟 ((UniformFun.gen (↑i : Type u_1) β ∘ V) i_1)))
  (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))
Tactic: simp_rw [iInf_uniformity, uniformity_comap,
    (UniformFun.hasBasis_uniformity_of_basis _ _ h).eq_biInf, comap_iInf, comap_principal,
    Function.comp_apply, UniformFun.gen, Subtype.forall, UniformOnFun.gen, preimage_setOf_eq,
    Prod.map_fst, Prod.map_snd, Function.comp_apply, UniformFun.toFun_ofFun, restrict_apply]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : UniformSpace β
𝔖 : Set (Set α)
hs : s ∈ 𝔖
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ Membership.mem (γ := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (𝓤 (α →ᵤ[𝔖] β)) (UniformOnFun.gen 𝔖 s V)
have rw : Membership.mem (γ := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V))
  (UniformOnFun.gen 𝔖 s V)
Tactic: rw [UniformOnFun.uniformity_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
f : α →ᵤ[𝔖] β
⊢ 𝓝 f =
    ⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {g : α →ᵤ[𝔖] β |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
have simp_rw : comap (Prod.mk f) (𝓤 (α →ᵤ[𝔖] β)) =
  ⨅ s ∈ 𝔖,
    ⨅ (i : ι),
      ⨅ (_ : p i),
        𝓟
          {g : α →ᵤ[𝔖] β |
            ∀ x ∈ s,
              Membership.mem (α := β × β) (V i)
                (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
Tactic: simp_rw [nhds_eq_comap_uniformity, UniformOnFun.uniformity_eq_of_basis _ _ h, comap_iInf,
    comap_principal, UniformOnFun.gen, preimage_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
f : α →ᵤ[𝔖] β
simp_rw :
  comap (Prod.mk f) (𝓤 (α →ᵤ[𝔖] β)) =
    ⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {g : α →ᵤ[𝔖] β |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
⊢ 𝓝 f =
    ⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {g : α →ᵤ[𝔖] β |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
have simp_rw₁ : Eq (α := Filter (α →ᵤ[𝔖] β)) (comap (Prod.mk f) (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))))
  (⨅ s ∈ 𝔖,
    ⨅ (i : ι),
      ⨅ (_ : p i),
        𝓟
          {g : α →ᵤ[𝔖] β |
            ∀ x ∈ s,
              Membership.mem (α := β × β) (V i)
                (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)})
Tactic: simp_rw [nhds_eq_comap_uniformity, UniformOnFun.uniformity_eq_of_basis _ _ h, comap_iInf,
    comap_principal, UniformOnFun.gen, preimage_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
f : α →ᵤ[𝔖] β
simp_rw :
  comap (Prod.mk f) (𝓤 (α →ᵤ[𝔖] β)) =
    ⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {g : α →ᵤ[𝔖] β |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
simp_rw₁ :
  Eq (α := Filter (α →ᵤ[𝔖] β)) (comap (Prod.mk f) (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))))
    (⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {g : α →ᵤ[𝔖] β |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)})
⊢ 𝓝 f =
    ⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {g : α →ᵤ[𝔖] β |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
have simp_rw₂ : Eq (α := Filter (α →ᵤ[𝔖] β)) (⨅ i ∈ 𝔖, ⨅ (i_1 : ι), ⨅ (_ : p i_1), comap (Prod.mk f) (𝓟 (UniformOnFun.gen 𝔖 i (V i_1))))
  (⨅ s ∈ 𝔖,
    ⨅ (i : ι),
      ⨅ (_ : p i),
        𝓟
          {g : α →ᵤ[𝔖] β |
            ∀ x ∈ s,
              Membership.mem (α := β × β) (V i)
                (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)})
Tactic: simp_rw [nhds_eq_comap_uniformity, UniformOnFun.uniformity_eq_of_basis _ _ h, comap_iInf,
    comap_principal, UniformOnFun.gen, preimage_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
f : α →ᵤ[𝔖] β
simp_rw :
  comap (Prod.mk f) (𝓤 (α →ᵤ[𝔖] β)) =
    ⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {g : α →ᵤ[𝔖] β |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
simp_rw₁ :
  Eq (α := Filter (α →ᵤ[𝔖] β)) (comap (Prod.mk f) (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))))
    (⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {g : α →ᵤ[𝔖] β |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)})
simp_rw₂ :
  Eq (α := Filter (α →ᵤ[𝔖] β))
    (⨅ i ∈ 𝔖, ⨅ (i_1 : ι), ⨅ (_ : p i_1), comap (Prod.mk f) (𝓟 (UniformOnFun.gen 𝔖 i (V i_1))))
    (⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {g : α →ᵤ[𝔖] β |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)})
⊢ 𝓝 f =
    ⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {g : α →ᵤ[𝔖] β |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
have simp_rw₃ : Eq (α := Filter (α →ᵤ[𝔖] β)) (⨅ i ∈ 𝔖, ⨅ (i_1 : ι), ⨅ (_ : p i_1), 𝓟 (Prod.mk f ⁻¹' UniformOnFun.gen 𝔖 i (V i_1)))
  (⨅ s ∈ 𝔖,
    ⨅ (i : ι),
      ⨅ (_ : p i),
        𝓟
          {g : α →ᵤ[𝔖] β |
            ∀ x ∈ s,
              Membership.mem (α := β × β) (V i)
                (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)})
Tactic: simp_rw [nhds_eq_comap_uniformity, UniformOnFun.uniformity_eq_of_basis _ _ h, comap_iInf,
    comap_principal, UniformOnFun.gen, preimage_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
f : α →ᵤ[𝔖] β
simp_rw :
  comap (Prod.mk f) (𝓤 (α →ᵤ[𝔖] β)) =
    ⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {g : α →ᵤ[𝔖] β |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
simp_rw₁ :
  Eq (α := Filter (α →ᵤ[𝔖] β)) (comap (Prod.mk f) (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))))
    (⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {g : α →ᵤ[𝔖] β |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)})
simp_rw₂ :
  Eq (α := Filter (α →ᵤ[𝔖] β))
    (⨅ i ∈ 𝔖, ⨅ (i_1 : ι), ⨅ (_ : p i_1), comap (Prod.mk f) (𝓟 (UniformOnFun.gen 𝔖 i (V i_1))))
    (⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {g : α →ᵤ[𝔖] β |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)})
simp_rw₃ :
  Eq (α := Filter (α →ᵤ[𝔖] β)) (⨅ i ∈ 𝔖, ⨅ (i_1 : ι), ⨅ (_ : p i_1), 𝓟 (Prod.mk f ⁻¹' UniformOnFun.gen 𝔖 i (V i_1)))
    (⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {g : α →ᵤ[𝔖] β |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)})
⊢ 𝓝 f =
    ⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {g : α →ᵤ[𝔖] β |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
have simp_rw₄ : Eq (α := Filter (α →ᵤ[𝔖] β))
  (⨅ i ∈ 𝔖,
    ⨅ (i_1 : ι),
      ⨅ (_ : p i_1),
        𝓟
          (Prod.mk f ⁻¹'
            {uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
              ∀ x ∈ i,
                Membership.mem (α := β × β) (V i_1)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) uv.1 x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) uv.2 x) : β × β)}))
  (⨅ s ∈ 𝔖,
    ⨅ (i : ι),
      ⨅ (_ : p i),
        𝓟
          {g : α →ᵤ[𝔖] β |
            ∀ x ∈ s,
              Membership.mem (α := β × β) (V i)
                (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)})
Tactic: simp_rw [nhds_eq_comap_uniformity, UniformOnFun.uniformity_eq_of_basis _ _ h, comap_iInf,
    comap_principal, UniformOnFun.gen, preimage_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : UniformSpace β
𝔖 : Set (Set α)
f : α →ᵤ[𝔖] β
hs : s ∈ 𝔖
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ {g : α →ᵤ[𝔖] β |
      ∀ x ∈ s,
        Membership.mem (α := β × β) V
          (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)} ∈
    𝓝 f
have rw : Membership.mem (γ := Filter (α →ᵤ[𝔖] β))
  (⨅ s ∈ 𝔖,
    ⨅ V ∈ 𝓤 β,
      𝓟
        {g : α →ᵤ[𝔖] β |
          ∀ x ∈ s,
            Membership.mem (α := β × β) V
              (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)})
  {g : α →ᵤ[𝔖] β |
    ∀ x ∈ s,
      Membership.mem (α := β × β) V
        (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
Tactic: rw [UniformOnFun.nhds_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
⊢ UniformContinuous (β := α →ᵤ[𝔖] β) fun (f : α →ᵤ β) ↦
    (ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) ((UniformFun.toFun : (a : α →ᵤ β) → α → β) f)
have simp : ∀ (i : Set α) (i_1 : i ∈ 𝔖) (i_2 : Set (β × β)) (i_3 : i_2 ∈ 𝓤 β),
  ∃ i_4 ∈ 𝓤 β,
    ∀ ⦃x : (α →ᵤ β) × (α →ᵤ β)⦄,
      x ∈ UniformFun.gen α β i_4 →
        Membership.mem (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (UniformOnFun.gen 𝔖 i i_2)
          (((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) ((UniformFun.toFun : (a : α →ᵤ β) → α → β) x.1),
              (ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) ((UniformFun.toFun : (a : α →ᵤ β) → α → β) x.2)) :
            (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
Tactic: simp only [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf, tendsto_principal,
    (UniformFun.hasBasis_uniformity _ _).eventually_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
h : univ ∈ 𝔖
⊢ UniformContinuous (β := α →ᵤ β) fun (f : α →ᵤ[𝔖] β) ↦
    (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)
have simp : ∀ i ∈ 𝓤 β,
  ∀ᶠ (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) in 𝓤 (α →ᵤ[𝔖] β),
    Membership.mem (α := (α →ᵤ β) × (α →ᵤ β)) (UniformFun.gen α β i)
      (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1),
          (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2)) :
        (α →ᵤ β) × (α →ᵤ β))
Tactic: simp only [UniformContinuous, (UniformFun.hasBasis_uniformity _ _).tendsto_right_iff]