awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
⊢ 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:
HasBasis.ext (HasBasis.iInf' fun i ↦ (basis_sets _).comap _)
    (UniformOnFun.hasBasis_uniformity α β _ ⟨∅, finite_empty⟩
      (directedOn_of_sup_mem fun _ _ ↦ .union))
    (fun ⟨S, U⟩ ⟨hS, hU⟩ ↦ ⟨⟨S, ⋂ x ∈ S, U x⟩, ⟨⟨hS, biInter_mem hS |>.mpr hU⟩,
      fun f hf ↦ mem_iInter₂.mpr fun x hx ↦ mem_iInter₂.mp (hf x hx) x hx⟩⟩)
    (fun ⟨S, U⟩ ⟨hS, hU⟩ ↦ ⟨⟨S, fun _ ↦ U⟩, ⟨hS, fun _ _ ↦ hU⟩, fun f hf x hx ↦
      mem_iInter₂.mp hf x hx⟩)

Premises used: Iff.mpr, Set.Finite.union, Set.finite_empty, UniformOnFun.gen, _private.0.UniformOnFun.isUniformEmbedding_toFun_finite.match_4, Set.iInter, uniformity, setOf, Set.mem_iInter₂, Set.Finite, Function.comp, Membership.mem, Exists, _private.0.UniformOnFun.isUniformEmbedding_toFun_finite.match_3, id, directedOn_of_sup_mem, Prod.mk, HasSubset.Subset, UniformOnFun.toFun, Prod.fst, Filter.HasBasis.comap, Filter.basis_sets, Filter.HasBasis.iInf', And, Set.preimage, And.intro, Filter.biInter_mem, Exists.intro, Iff.mp, _private.0.UniformOnFun.isUniformEmbedding_toFun_finite.match_2, Filter.HasBasis.ext, EmptyCollection.emptyCollection, Prod.snd, _private.0.UniformOnFun.isUniformEmbedding_toFun_finite.match_1, DFunLike.coe, UniformOnFun.hasBasis_uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
⊢ 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:
refine HasBasis.ext (HasBasis.iInf' fun i ↦ (basis_sets _).comap _)
    (UniformOnFun.hasBasis_uniformity α β _ ⟨∅, finite_empty⟩
      (directedOn_of_sup_mem fun _ _ ↦ .union))
    (fun ⟨S, U⟩ ⟨hS, hU⟩ ↦ ⟨⟨S, ⋂ x ∈ S, U x⟩, ⟨⟨hS, biInter_mem hS |>.mpr hU⟩,
      fun f hf ↦ mem_iInter₂.mpr fun x hx ↦ mem_iInter₂.mp (hf x hx) x hx⟩⟩)
    (fun ⟨S, U⟩ ⟨hS, hU⟩ ↦ ⟨⟨S, fun _ ↦ U⟩, ⟨hS, fun _ _ ↦ hU⟩, fun f hf x hx ↦
      mem_iInter₂.mp hf x hx⟩)

Premises used: Iff.mpr, UniformOnFun.gen, Set.iInter, uniformity, Set.mem_iInter₂, Membership.mem, Exists, id, directedOn_of_sup_mem, Prod.mk, HasSubset.Subset, UniformOnFun.toFun, Prod.fst, Filter.HasBasis.comap, Filter.basis_sets, Filter.HasBasis.iInf', And, Set.preimage, And.intro, Filter.biInter_mem, Exists.intro, Iff.mp, _private.0.UniformOnFun.isUniformEmbedding_toFun_finite.match_2, Filter.HasBasis.ext, EmptyCollection.emptyCollection, Prod.snd, _private.0.UniformOnFun.isUniformEmbedding_toFun_finite.match_1, DFunLike.coe, UniformOnFun.hasBasis_uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
⊢ IsEmbedding (X := α →ᵤ[{s : Set α | s.Finite}] β) (Y := α → β)
    (⇑(toFun {s : Set α | s.Finite}) : (a : α →ᵤ[{s : Set α | s.Finite}] β) → α → β)

Tactic:
(isUniformEmbedding_toFun_finite α β).isEmbedding

Premises used: IsUniformEmbedding.isEmbedding, UniformOnFun.isUniformEmbedding_toFun_finite
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
⊢ Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (𝓤 (α →ᵤ[𝔖] β)) (⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V))

Tactic:
UniformOnFun.uniformity_eq_of_basis _ _ (𝓤 β).basis_sets

Premises used: UniformOnFun.uniformity_eq_of_basis, uniformity, Filter.basis_sets
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : UniformSpace β
𝔖 : Set (Set α)
hs : s ∈ 𝔖
V : Set (β × β)
hV : V ∈ 𝓤 β
rw :
  Membership.mem (γ := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V))
    (UniformOnFun.gen 𝔖 s V)
⊢ Membership.mem (γ := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (𝓤 (α →ᵤ[𝔖] β)) (UniformOnFun.gen 𝔖 s V)

Tactic:
rw [UniformOnFun.uniformity_eq]

Premises used: UniformOnFun.uniformity_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : UniformSpace β
𝔖 : Set (Set α)
hs : s ∈ 𝔖
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ Membership.mem (γ := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V))
    (UniformOnFun.gen 𝔖 s V)

Tactic:
apply_rules [mem_iInf_of_mem, mem_principal_self]

Premises used: Filter.mem_principal_self, Filter.mem_iInf_of_mem
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
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) : β × β)})
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) : β × β)})
⊢ 𝓝 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]

Premises used: UniformOnFun.uniformity_eq_of_basis, UniformOnFun.gen, Filter.comap_iInf, Set.preimage_setOf_eq, Filter.comap_principal, nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
f : α →ᵤ[𝔖] β
⊢ 𝓝 f =
    ⨅ s ∈ 𝔖,
      ⨅ V ∈ 𝓤 β,
        𝓟
          {g : α →ᵤ[𝔖] β |
            ∀ x ∈ s,
              Membership.mem (α := β × β) V
                (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}

Tactic:
UniformOnFun.nhds_eq_of_basis _ _ (𝓤 β).basis_sets f

Premises used: Set.Mem, UniformOnFun.nhds_eq_of_basis, uniformity, setOf, Filter.basis_sets
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : UniformSpace β
𝔖 : Set (Set α)
f : α →ᵤ[𝔖] β
hs : s ∈ 𝔖
V : Set (β × β)
hV : V ∈ 𝓤 β
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) : β × β)}
⊢ {g : α →ᵤ[𝔖] β |
      ∀ x ∈ s,
        Membership.mem (α := β × β) V
          (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)} ∈
    𝓝 f

Tactic:
rw [UniformOnFun.nhds_eq]

Premises used: UniformOnFun.nhds_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : UniformSpace β
𝔖 : Set (Set α)
f : α →ᵤ[𝔖] β
hs : s ∈ 𝔖
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ 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:
apply_rules [mem_iInf_of_mem, mem_principal_self]

Premises used: Filter.mem_principal_self, Filter.mem_iInf_of_mem
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
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)) :
              (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
⊢ UniformContinuous (β := α →ᵤ[𝔖] β) fun (f : α →ᵤ β) ↦
    (ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) ((UniformFun.toFun : (a : α →ᵤ β) → α → β) f)

Tactic:
simp only [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf, tendsto_principal,
    (UniformFun.hasBasis_uniformity _ _).eventually_iff]

Premises used: UniformContinuous, UniformFun.hasBasis_uniformity, Filter.tendsto_principal, Filter.HasBasis.eventually_iff, Filter.tendsto_iInf, UniformOnFun.uniformity_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
⊢ ∀ (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:
fun _ _ U hU ↦ ⟨U, hU, fun f hf x _ ↦ hf x⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
⊢ ∀ (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:
exact fun _ _ U hU ↦ ⟨U, hU, fun f hf x _ ↦ hf x⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
h : univ ∈ 𝔖
simp :
  ∀ i ∈ 𝓤 β,
    ∀ᶠ (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) in 𝓤 (α →ᵤ[𝔖] β),
      Membership.mem (α := (α →ᵤ β) × (α →ᵤ β)) (UniformFun.gen α β i)
        (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1),
            (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2)) :
          (α →ᵤ β) × (α →ᵤ β))
⊢ UniformContinuous (β := α →ᵤ β) fun (f : α →ᵤ[𝔖] β) ↦
    (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)

Tactic:
simp only [UniformContinuous, (UniformFun.hasBasis_uniformity _ _).tendsto_right_iff]

Premises used: UniformContinuous, UniformFun.hasBasis_uniformity, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
h : univ ∈ 𝔖
U : Set (β × β)
hU : U ∈ 𝓤 β
f : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)
hf : f ∈ UniformOnFun.gen 𝔖 univ U
x : α
⊢ Membership.mem (α := β × β) U
    (((UniformFun.toFun : (a : α →ᵤ β) → α → β)
          (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.1),
                (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.2)).1 :
            α →ᵤ β)
          x,
        (UniformFun.toFun : (a : α →ᵤ β) → α → β)
          (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.1),
                (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.2)).2 :
            α →ᵤ β)
          x) :
      β × β)

Tactic:
hf x (mem_univ _)

Premises used: Set.Mem, Set.mem_univ
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
h : univ ∈ 𝔖
U : Set (β × β)
hU : U ∈ 𝓤 β
h₁ :
  ∀ (a : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)),
    Membership.mem (γ := Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
      {x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
        x ∈ UniformOnFun.gen 𝔖 univ U →
          Membership.mem (γ := Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
            {x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
              (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
                  Membership.mem (α := (α →ᵤ β) × (α →ᵤ β)) (UniformFun.gen α β U)
                    (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1),
                        (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2)) :
                      (α →ᵤ β) × (α →ᵤ β)))
                x}
            x}
      a
h₂ :
  ∀ a ∈ UniformOnFun.gen 𝔖 univ U,
    Membership.mem (α := (α →ᵤ β) × (α →ᵤ β)) (UniformFun.gen α β U)
      (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) a.1),
          (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) a.2)) :
        (α →ᵤ β) × (α →ᵤ β))
h₃ :
  ∀ (f : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (hf : f ∈ UniformOnFun.gen 𝔖 univ U) (x : α),
    Membership.mem (α := β × β) U
      (((UniformFun.toFun : (a : α →ᵤ β) → α → β)
            (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.1),
                  (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.2)).1 :
              α →ᵤ β)
            x,
          (UniformFun.toFun : (a : α →ᵤ β) → α → β)
            (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.1),
                  (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f.2)).2 :
              α →ᵤ β)
            x) :
        β × β)
⊢ ∀ᶠ (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) in 𝓤 (α →ᵤ[𝔖] β),
    Membership.mem (α := (α →ᵤ β) × (α →ᵤ β)) (UniformFun.gen α β U)
      (((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1),
          (UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2)) :
        (α →ᵤ β) × (α →ᵤ β))

Tactic:
filter_upwards [UniformOnFun.gen_mem_uniformity _ _ h hU] with f hf x using hf x (mem_univ _)

Premises used: UniformOnFun.gen_mem_uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
simp :
  Tendsto (β := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
    (fun (x : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)) ↦
      (Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.1,
        Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.2))
    (⨅ i₂ ∈ 𝓤 β, ⨅ i₁ ∈ 𝔗, 𝓟 (UniformOnFun.gen 𝔗 i₁ i₂)) (⨅ i₂ ∈ 𝓤 β, ⨅ i₁ ∈ 𝔖, 𝓟 (UniformOnFun.gen 𝔖 i₁ i₂))
⊢ UniformContinuous (α := α →ᵤ[𝔗] β) (β := α →ᵤ[𝔖] β)
    (Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β))

Tactic:
simp only [UniformContinuous, UniformOnFun.uniformity_eq, iInf₂_comm (ι₂ := Set (β × β))]

Premises used: UniformContinuous, iInf₂_comm, UniformOnFun.uniformity_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
⊢ Tendsto (β := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
    (fun (x : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)) ↦
      (Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.1,
        Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.2))
    (⨅ i₂ ∈ 𝓤 β, ⨅ i₁ ∈ 𝔗, 𝓟 (UniformOnFun.gen 𝔗 i₁ i₂)) (⨅ i₂ ∈ 𝓤 β, ⨅ i₁ ∈ 𝔖, 𝓟 (UniformOnFun.gen 𝔖 i₁ i₂))

Tactic:
tendsto_iInf_iInf fun V ↦ tendsto_iInf_iInf fun hV ↦ ?_

Premises used: Filter.tendsto_iInf_iInf
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
refine :
  ∀ (V : Set (β × β)) (hV : V ∈ 𝓤 β),
    Tendsto (β := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
      (fun (x : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)) ↦
        (Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.1,
          Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.2))
      (⨅ i₁ ∈ 𝔗, 𝓟 (UniformOnFun.gen 𝔗 i₁ V)) (⨅ i₁ ∈ 𝔖, 𝓟 (UniformOnFun.gen 𝔖 i₁ V))
⊢ Tendsto (β := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
    (fun (x : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)) ↦
      (Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.1,
        Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.2))
    (⨅ i₂ ∈ 𝓤 β, ⨅ i₁ ∈ 𝔗, 𝓟 (UniformOnFun.gen 𝔗 i₁ i₂)) (⨅ i₂ ∈ 𝓤 β, ⨅ i₁ ∈ 𝔖, 𝓟 (UniformOnFun.gen 𝔖 i₁ i₂))

Tactic:
refine tendsto_iInf_iInf fun V ↦ tendsto_iInf_iInf fun hV ↦ ?_

Premises used: Filter.tendsto_iInf_iInf
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
simp :
  ∀ (i : Set α) (i_1 : i ∈ 𝔖),
    ∃ (I : Set (Set α)),
      I.Finite ∧
        (∀ i ∈ I, i ∈ 𝔗) ∧
          Subset (α := Set ((α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β))) (⋂ i ∈ I, UniformOnFun.gen 𝔗 i V)
            {x : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β) |
              (Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)
                    x.1,
                  Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β)
                    (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.2) ∈
                UniformOnFun.gen 𝔖 i V}
⊢ Tendsto (β := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
    (fun (x : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β)) ↦
      (Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.1,
        Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.2))
    (⨅ i₁ ∈ 𝔗, 𝓟 (UniformOnFun.gen 𝔗 i₁ V)) (⨅ i₁ ∈ 𝔖, 𝓟 (UniformOnFun.gen 𝔖 i₁ V))

Tactic:
simp only [tendsto_iInf, tendsto_principal, Filter.Eventually, mem_biInf_principal]

Premises used: Filter.Eventually, Filter.tendsto_principal, Filter.mem_biInf_principal, Filter.tendsto_iInf
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
s : Set α
hs : s ∈ 𝔖
obtain :
  ∀ (T : Set (Set α)) (hT𝔗 : T ⊆ 𝔗) (hT : T.Finite) (hsT : s ⊆ ⋃₀ T),
    ∃ (I : Set (Set α)),
      I.Finite ∧
        (∀ i ∈ I, i ∈ 𝔗) ∧
          Subset (α := Set ((α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β))) (⋂ i ∈ I, UniformOnFun.gen 𝔗 i V)
            {x : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β) |
              (Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)
                    x.1,
                  Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β)
                    (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x.2) ∈
                UniformOnFun.gen 𝔖 s V}
⊢ ∃ (I : Set (Set α)),
    I.Finite ∧
      (∀ i ∈ I, i ∈ 𝔗) ∧
        Subset (α := Set ((α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β))) (⋂ i ∈ I, UniformOnFun.gen 𝔗 i V)
          {x : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β) |
            (Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)
                  x.1,
                Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)
                  x.2) ∈
              UniformOnFun.gen 𝔖 s V}

Tactic:
obtain ⟨T, hT𝔗, hT, hsT⟩ := h s hs
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
s : Set α
hs : s ∈ 𝔖
T : Set (Set α)
hT𝔗 : T ⊆ 𝔗
hT : T.Finite
hsT : s ⊆ ⋃₀ T
⊢ ∃ (I : Set (Set α)),
    I.Finite ∧
      (∀ i ∈ I, i ∈ 𝔗) ∧
        Subset (α := Set ((α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β))) (⋂ i ∈ I, UniformOnFun.gen 𝔗 i V)
          {x : (α →ᵤ[𝔗] β) × (α →ᵤ[𝔗] β) |
            (Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)
                  x.1,
                Function.comp (β := α → β) (⇑(ofFun 𝔗) : (a : α → β) → α →ᵤ[𝔗] β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)
                  x.2) ∈
              UniformOnFun.gen 𝔖 s V}

Tactic:
⟨T, hT, hT𝔗, fun f hf ↦ ?_⟩

Premises used: And.intro, Exists.intro