awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
I : Set ι
I_finite : I.Finite
I_cover : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, range (φ i)) univ
⊢ LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β)))
    (⨅ (i : ι),
      comap (β := UniformFun.{u_6, u_2} (δ i) β × UniformFun.{u_6, u_2} (δ i) β)
        (Prod.map
          (Function.comp (β := δ i → β) (⇑ofFun : (a : δ i → β) → δ i →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
          (Function.comp (β := δ i → β) (⇑ofFun : (a : δ i → β) → δ i →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑toFun : (a : α →ᵤ β) → α → β))))
        (𝓤 (UniformFun.{u_6, u_2} (δ i) β)))
    (𝓤 (α →ᵤ β))

Tactic:
HasBasis.iInf (fun i : ι ↦ UniformFun.hasBasis_uniformity (δ i) β |>.comap _)
      |>.le_basis_iff (UniformFun.hasBasis_uniformity α β) |>.mpr fun U hU ↦
    ⟨⟨I, fun _ ↦ U⟩, ⟨I_finite, fun _ ↦ hU⟩, fun ⟨f, g⟩ hfg x ↦ ?_⟩

Premises used: Iff.mpr, Filter.HasBasis.iInf, Set.Mem, UniformFun.hasBasis_uniformity, setOf, Membership.mem, Filter.HasBasis.le_basis_iff, Prod.mk, UniformFun.toFun, Prod.fst, Filter.HasBasis.comap, _private.0.UniformFun.uniformSpace_eq_iInf_precomp_of_cover.match_1, And.intro, Exists.intro, Sigma.mk, Prod.snd, DFunLike.coe
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
I : Set ι
I_finite : I.Finite
I_cover : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, range (φ i)) univ
h :
  ∀ (U : Set (β × β)) (hU : U ∈ 𝓤 β) (x : (α →ᵤ β) × (α →ᵤ β)) (x : α) (f g : α →ᵤ β)
    (hfg :
      Membership.mem (γ := Set ((α →ᵤ β) × (α →ᵤ β)))
        (⋂ (i :
          (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β))
                (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β)) I fun (x : (↑I : Type u_4)) ↦
                  U)) :
            Type u_4)),
          preimage (β := UniformFun.{u_6, u_2} (δ (↑i : ι)) β × UniformFun.{u_6, u_2} (δ (↑i : ι)) β)
            (Prod.map
              (Function.comp (β := δ (↑i : ι) → β) (⇑ofFun : (a : δ (↑i : ι) → β) → δ (↑i : ι) →ᵤ β)
                ((fun (x : α → β) ↦ x ∘ φ (↑i : ι)) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
              (Function.comp (β := δ (↑i : ι) → β) (⇑ofFun : (a : δ (↑i : ι) → β) → δ (↑i : ι) →ᵤ β)
                ((fun (x : α → β) ↦ x ∘ φ (↑i : ι)) ∘ (⇑toFun : (a : α →ᵤ β) → α → β))))
            (UniformFun.gen (δ (↑i : ι)) β
              (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β))
                (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β)) I fun (x : (↑I : Type u_4)) ↦ U)
                i)))
        (f, g)),
    Membership.mem (α := β × β) U
      (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 x, (toFun : (a : α →ᵤ β) → α → β) (f, g).2 x) : β × β)
⊢ LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β)))
    (⨅ (i : ι),
      comap (β := UniformFun.{u_6, u_2} (δ i) β × UniformFun.{u_6, u_2} (δ i) β)
        (Prod.map
          (Function.comp (β := δ i → β) (⇑ofFun : (a : δ i → β) → δ i →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
          (Function.comp (β := δ i → β) (⇑ofFun : (a : δ i → β) → δ i →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑toFun : (a : α →ᵤ β) → α → β))))
        (𝓤 (UniformFun.{u_6, u_2} (δ i) β)))
    (𝓤 (α →ᵤ β))

Tactic:
refine HasBasis.iInf (fun i : ι ↦ UniformFun.hasBasis_uniformity (δ i) β |>.comap _)
      |>.le_basis_iff (UniformFun.hasBasis_uniformity α β) |>.mpr fun U hU ↦
    ⟨⟨I, fun _ ↦ U⟩, ⟨I_finite, fun _ ↦ hU⟩, fun ⟨f, g⟩ hfg x ↦ ?_⟩

Premises used: Iff.mpr, Filter.HasBasis.iInf, UniformFun.hasBasis_uniformity, Filter.HasBasis.le_basis_iff, Filter.HasBasis.comap, And.intro, Exists.intro, Sigma.mk
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
I : Set ι
I_finite : I.Finite
I_cover : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, range (φ i)) univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x_1 : (α →ᵤ β) × (α →ᵤ β)
x : α
f g : α →ᵤ β
hfg :
  Membership.mem (γ := Set ((α →ᵤ β) × (α →ᵤ β)))
    (⋂ (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β)) I fun (x : (↑I : Type u_4)) ↦ U)) :
        Type u_4)),
      preimage (β := UniformFun.{u_6, u_2} (δ (↑i : ι)) β × UniformFun.{u_6, u_2} (δ (↑i : ι)) β)
        (Prod.map
          (Function.comp (β := δ (↑i : ι) → β) (⇑ofFun : (a : δ (↑i : ι) → β) → δ (↑i : ι) →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ (↑i : ι)) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
          (Function.comp (β := δ (↑i : ι) → β) (⇑ofFun : (a : δ (↑i : ι) → β) → δ (↑i : ι) →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ (↑i : ι)) ∘ (⇑toFun : (a : α →ᵤ β) → α → β))))
        (UniformFun.gen (δ (↑i : ι)) β
          (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β)) I fun (x : (↑I : Type u_4)) ↦ U) i)))
    (f, g)
h :
  ∀ (i : ι) (hi : i ∈ I) (y : δ i),
    Membership.mem (α := β × β) U
      (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 (φ i y), (toFun : (a : α →ᵤ β) → α → β) (f, g).2 (φ i y)) : β × β)
⊢ Membership.mem (α := β × β) U
    (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 x, (toFun : (a : α →ᵤ β) → α → β) (f, g).2 x) : β × β)

Tactic:
rcases mem_iUnion₂.mp <| I_cover.ge <| mem_univ x with ⟨i, hi, y, rfl⟩

Premises used: Eq.ge, Set.mem_iUnion₂, Iff.mp, Set.mem_univ, rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
I : Set ι
I_finite : I.Finite
I_cover : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, range (φ i)) univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x : (α →ᵤ β) × (α →ᵤ β)
f g : α →ᵤ β
hfg :
  Membership.mem (γ := Set ((α →ᵤ β) × (α →ᵤ β)))
    (⋂ (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β)) I fun (x : (↑I : Type u_4)) ↦ U)) :
        Type u_4)),
      preimage (β := UniformFun.{u_6, u_2} (δ (↑i : ι)) β × UniformFun.{u_6, u_2} (δ (↑i : ι)) β)
        (Prod.map
          (Function.comp (β := δ (↑i : ι) → β) (⇑ofFun : (a : δ (↑i : ι) → β) → δ (↑i : ι) →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ (↑i : ι)) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
          (Function.comp (β := δ (↑i : ι) → β) (⇑ofFun : (a : δ (↑i : ι) → β) → δ (↑i : ι) →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ (↑i : ι)) ∘ (⇑toFun : (a : α →ᵤ β) → α → β))))
        (UniformFun.gen (δ (↑i : ι)) β
          (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β)) I fun (x : (↑I : Type u_4)) ↦ U) i)))
    (f, g)
i : ι
hi : i ∈ I
y : δ i
⊢ Membership.mem (α := β × β) U
    (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 (φ i y), (toFun : (a : α →ᵤ β) → α → β) (f, g).2 (φ i y)) : β × β)

Tactic:
mem_iInter.mp hfg ⟨i, hi⟩ y

Premises used: Set.Mem, Set.mem_iInter, Subtype.mk, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
I : Set ι
I_finite : I.Finite
I_cover : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, range (φ i)) univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x : (α →ᵤ β) × (α →ᵤ β)
f g : α →ᵤ β
hfg :
  Membership.mem (γ := Set ((α →ᵤ β) × (α →ᵤ β)))
    (⋂ (i :
      (↑(Sigma.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β)) I fun (x : (↑I : Type u_4)) ↦ U)) :
        Type u_4)),
      preimage (β := UniformFun.{u_6, u_2} (δ (↑i : ι)) β × UniformFun.{u_6, u_2} (δ (↑i : ι)) β)
        (Prod.map
          (Function.comp (β := δ (↑i : ι) → β) (⇑ofFun : (a : δ (↑i : ι) → β) → δ (↑i : ι) →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ (↑i : ι)) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
          (Function.comp (β := δ (↑i : ι) → β) (⇑ofFun : (a : δ (↑i : ι) → β) → δ (↑i : ι) →ᵤ β)
            ((fun (x : α → β) ↦ x ∘ φ (↑i : ι)) ∘ (⇑toFun : (a : α →ᵤ β) → α → β))))
        (UniformFun.gen (δ (↑i : ι)) β
          (Sigma.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β))
            (Sigma.mk (β := fun (I : Set ι) ↦ (i : (↑I : Type u_4)) → Set (β × β)) I fun (x : (↑I : Type u_4)) ↦ U) i)))
    (f, g)
i : ι
hi : i ∈ I
y : δ i
⊢ Membership.mem (α := β × β) U
    (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 (φ i y), (toFun : (a : α →ᵤ β) → α → β) (f, g).2 (φ i y)) : β × β)

Tactic:
exact mem_iInter.mp hfg ⟨i, hi⟩ y

Premises used: Set.mem_iInter, Subtype.mk, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
S : Set α
V : Set (β × β)
h :
  ∀ (uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)),
    uv ∈ UniformOnFun.gen 𝔖 S V ↔
      Membership.mem (γ := Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
        (preimage (β := ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
          (Prod.map
              (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
                (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
              (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
                (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β)) :
            (α →ᵤ β) × (α →ᵤ β) → ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
          (UniformFun.gen (↑S : Type u_1) β V :
            Set (UniformFun.{u_1, u_2} (↑S : Type u_1) β × UniformFun.{u_1, u_2} (↑S : Type u_1) β)))
        uv
⊢ UniformOnFun.gen 𝔖 S V =
    preimage (β := ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
      (Prod.map
          (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
            (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
          (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
            (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β)) :
        (α →ᵤ β) × (α →ᵤ β) → ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
      (UniformFun.gen (↑S : Type u_1) β V :
        Set (UniformFun.{u_1, u_2} (↑S : Type u_1) β × UniformFun.{u_1, u_2} (↑S : Type u_1) β))

Tactic:
ext uv
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
S : Set α
V : Set (β × β)
uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)
⊢ uv ∈ UniformOnFun.gen 𝔖 S V ↔
    Membership.mem (γ := Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
      (preimage (β := ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
        (Prod.map
            (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
              (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
            (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
              (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β)) :
          (α →ᵤ β) × (α →ᵤ β) → ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
        (UniformFun.gen (↑S : Type u_1) β V :
          Set (UniformFun.{u_1, u_2} (↑S : Type u_1) β × UniformFun.{u_1, u_2} (↑S : Type u_1) β)))
      uv

Tactic:
⟨fun h ⟨x, hx⟩ => h x hx, fun h x hx => h ⟨x, hx⟩⟩

Premises used: Function.comp, Membership.mem, Prod.mk, Prod.map, UniformFun.toFun, Prod.fst, Subtype.mk, Iff.intro, _private.0.UniformOnFun.gen_eq_preimage_restrict.match_1, Set.restrict, Prod.snd, DFunLike.coe
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
S : Set α
V : Set (β × β)
uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)
⊢ uv ∈ UniformOnFun.gen 𝔖 S V ↔
    Membership.mem (γ := Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
      (preimage (β := ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
        (Prod.map
            (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
              (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
            (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
              (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β)) :
          (α →ᵤ β) × (α →ᵤ β) → ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
        (UniformFun.gen (↑S : Type u_1) β V :
          Set (UniformFun.{u_1, u_2} (↑S : Type u_1) β × UniformFun.{u_1, u_2} (↑S : Type u_1) β)))
      uv

Tactic:
exact ⟨fun h ⟨x, hx⟩ => h x hx, fun h x hx => h ⟨x, hx⟩⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
S S' : Set α
V V' : Set (β × β)
hS : S' ⊆ S
hV : V ⊆ V'
⊢ UniformOnFun.gen 𝔖 S V ⊆ UniformOnFun.gen 𝔖 S' V'

Tactic:
fun _uv h x hx => hV (h x <| hS hx)

Premises used: UniformOnFun.gen, Set.Mem, setOf, Set.Subset
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
h : 𝔖.Nonempty
h' : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
𝓑 : FilterBasis (β × β)
⊢ IsBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (fun (SV : Prod.{u_1, u_2} (Set α) (Set (β × β))) ↦ SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓑)
    fun (SV : Prod.{u_1, u_2} (Set α) (Set (β × β))) ↦ UniformOnFun.gen 𝔖 SV.1 SV.2

Tactic:
⟨h.prod 𝓑.nonempty, fun {U₁V₁ U₂V₂} h₁ h₂ =>
    let ⟨U₃, hU₃, hU₁₃, hU₂₃⟩ := h' U₁V₁.1 h₁.1 U₂V₂.1 h₂.1
    let ⟨V₃, hV₃, hV₁₂₃⟩ := 𝓑.inter_sets h₁.2 h₂.2
    ⟨⟨U₃, V₃⟩,
      ⟨⟨hU₃, hV₃⟩, fun _ H =>
        ⟨fun x hx => (hV₁₂₃ <| H x <| hU₁₃ hx).1, fun x hx => (hV₁₂₃ <| H x <| hU₂₃ hx).2⟩⟩⟩⟩

Premises used: UniformOnFun.gen, Membership.mem, Exists, Filter.IsBasis.mk, FilterBasis.inter_sets, Prod.mk, HasSubset.Subset, _private.0.UniformOnFun.isBasis_gen.match_2, Prod.fst, Inter.inter, And, _private.0.UniformOnFun.isBasis_gen.match_1, Set.Nonempty.prod, And.right, And.left, And.intro, Exists.intro, FilterBasis.nonempty, Prod.snd
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
simp :
  Eq (α := TopologicalSpace (α →ᵤ[𝔖] β)) (⨅ i ∈ 𝔖, UniformSpace.toTopologicalSpace)
    (⨅ s ∈ 𝔖,
      TopologicalSpace.induced (Y := UniformFun.{u_1, u_2} (↑s : Type u_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 (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
            (α →ᵤ[𝔖] β) → (↑s : Type u_1) → β))
        (UniformFun.topologicalSpace (↑s : Type u_1) β))
⊢ topologicalSpace α β 𝔖 =
    ⨅ s ∈ 𝔖,
      TopologicalSpace.induced (Y := UniformFun.{u_1, u_2} (↑s : Type u_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 (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
            (α →ᵤ[𝔖] β) → (↑s : Type u_1) → β))
        (UniformFun.topologicalSpace (↑s : Type u_1) β)

Tactic:
simp only [UniformOnFun.topologicalSpace, UniformSpace.toTopologicalSpace_iInf]

Premises used: UniformOnFun.topologicalSpace, UniformSpace.toTopologicalSpace_iInf
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
⊢ Eq (α := TopologicalSpace (α →ᵤ[𝔖] β)) (⨅ i ∈ 𝔖, UniformSpace.toTopologicalSpace)
    (⨅ s ∈ 𝔖,
      TopologicalSpace.induced (Y := UniformFun.{u_1, u_2} (↑s : Type u_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 (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
            (α →ᵤ[𝔖] β) → (↑s : Type u_1) → β))
        (UniformFun.topologicalSpace (↑s : Type u_1) β))

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
S : Set α
simp_rw :
  HasBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
    (comap (Prod.map (S.restrict (π := fun (a : α) ↦ β)) (S.restrict (π := fun (a : α) ↦ β)))
      (𝓤 ((a : (↑S : Type u_1)) → β)))
    p fun (i : ι) ↦
    preimage (β := ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
      (Prod.map
          (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
            (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
          (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
            (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β)) :
        (α →ᵤ β) × (α →ᵤ β) → ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
      (UniformFun.gen (↑S : Type u_1) β (s i) :
        Set (UniformFun.{u_1, u_2} (↑S : Type u_1) β × UniformFun.{u_1, u_2} (↑S : Type u_1) β))
⊢ HasBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (𝓤 (α →ᵤ[𝔖] β)) p fun (i : ι) ↦ UniformOnFun.gen 𝔖 S (s i)

Tactic:
simp_rw [UniformOnFun.gen_eq_preimage_restrict, uniformity_comap]

Premises used: UniformOnFun.gen_eq_preimage_restrict, uniformity_comap
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
S : Set α
⊢ HasBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
    (comap (Prod.map (S.restrict (π := fun (a : α) ↦ β)) (S.restrict (π := fun (a : α) ↦ β)))
      (𝓤 ((a : (↑S : Type u_1)) → β)))
    p fun (i : ι) ↦
    preimage (β := ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
      (Prod.map
          (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
            (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
          (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
            (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β)) :
        (α →ᵤ β) × (α →ᵤ β) → ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
      (UniformFun.gen (↑S : Type u_1) β (s i) :
        Set (UniformFun.{u_1, u_2} (↑S : Type u_1) β × UniformFun.{u_1, u_2} (↑S : Type u_1) β))

Tactic:
(UniformFun.hasBasis_uniformity_of_basis S β hb).comap _

Premises used: setOf, Set.Elem, UniformFun.gen, UniformFun.hasBasis_uniformity_of_basis, Filter.HasBasis.comap, UniformFun, UniformOnFun, Set.restrict
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
S : Set α
⊢ HasBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
    (comap (Prod.map (S.restrict (π := fun (a : α) ↦ β)) (S.restrict (π := fun (a : α) ↦ β)))
      (𝓤 ((a : (↑S : Type u_1)) → β)))
    p fun (i : ι) ↦
    preimage (β := ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
      (Prod.map
          (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
            (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
          (Function.comp (β := (a : α) → β) (S.restrict (π := fun (a : α) ↦ β))
            (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β)) :
        (α →ᵤ β) × (α →ᵤ β) → ((a : (↑S : Type u_1)) → β) × ((a : (↑S : Type u_1)) → β))
      (UniformFun.gen (↑S : Type u_1) β (s i) :
        Set (UniformFun.{u_1, u_2} (↑S : Type u_1) β × UniformFun.{u_1, u_2} (↑S : Type u_1) β))

Tactic:
exact (UniformFun.hasBasis_uniformity_of_basis S β hb).comap _

Premises used: Set.Elem, UniformFun.hasBasis_uniformity_of_basis, Filter.HasBasis.comap
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
h : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
⊢ DirectedOn
    (Order.Preimage (β := UniformSpace ((a : α) → β))
      (fun (s : Set α) ↦
        UniformSpace.comap (s.restrict (π := fun (a : α) ↦ β)) (UniformFun.uniformSpace (↑s : Type u_1) β))
      GE.ge)
    𝔖

Tactic:
h.mono fun _ _ hst =>
    ((UniformOnFun.hasBasis_uniformity_of_basis_aux₁ α β 𝔖 hb _).le_basis_iff
          (UniformOnFun.hasBasis_uniformity_of_basis_aux₁ α β 𝔖 hb _)).mpr
      fun V hV => ⟨V, hV, UniformOnFun.gen_mono hst subset_rfl⟩

Premises used: Iff.mpr, UniformOnFun.gen_mono, Filter.HasBasis.le_basis_iff, DirectedOn.mono, And.intro, Exists.intro, UniformOnFun.hasBasis_uniformity_of_basis_aux₁, subset_rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
h : 𝔖.Nonempty
h' : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
simp :
  HasBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β))
    (fun (Si : Prod.{u_1, u_4} (Set α) ι) ↦ Si.1 ∈ 𝔖 ∧ p Si.2) fun (Si : Prod.{u_1, u_4} (Set α) ι) ↦
    UniformOnFun.gen 𝔖 Si.1 (s Si.2)
⊢ HasBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (𝓤 (α →ᵤ[𝔖] β)) (fun (Si : Prod.{u_1, u_4} (Set α) ι) ↦ Si.1 ∈ 𝔖 ∧ p Si.2)
    fun (Si : Prod.{u_1, u_4} (Set α) ι) ↦ UniformOnFun.gen 𝔖 Si.1 (s Si.2)

Tactic:
simp only [iInf_uniformity]

Premises used: iInf_uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
h : 𝔖.Nonempty
h' : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
⊢ HasBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β))
    (fun (Si : Prod.{u_1, u_4} (Set α) ι) ↦ Si.1 ∈ 𝔖 ∧ p Si.2) fun (Si : Prod.{u_1, u_4} (Set α) ι) ↦
    UniformOnFun.gen 𝔖 Si.1 (s Si.2)

Tactic:
hasBasis_biInf_of_directed h (fun S => UniformOnFun.gen 𝔖 S ∘ s) _
      (fun S _hS => UniformOnFun.hasBasis_uniformity_of_basis_aux₁ α β 𝔖 hb S)
      (UniformOnFun.hasBasis_uniformity_of_basis_aux₂ α β 𝔖 h' hb)

Premises used: UniformOnFun.gen, Filter.hasBasis_biInf_of_directed, setOf, Function.comp, UniformFun, UniformOnFun, Set.restrict, UniformOnFun.hasBasis_uniformity_of_basis_aux₁, UniformOnFun.hasBasis_uniformity_of_basis_aux₂
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
h : 𝔖.Nonempty
h' : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
⊢ HasBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β))
    (fun (Si : Prod.{u_1, u_4} (Set α) ι) ↦ Si.1 ∈ 𝔖 ∧ p Si.2) fun (Si : Prod.{u_1, u_4} (Set α) ι) ↦
    UniformOnFun.gen 𝔖 Si.1 (s Si.2)

Tactic:
exact
    hasBasis_biInf_of_directed h (fun S => UniformOnFun.gen 𝔖 S ∘ s) _
      (fun S _hS => UniformOnFun.hasBasis_uniformity_of_basis_aux₁ α β 𝔖 hb S)
      (UniformOnFun.hasBasis_uniformity_of_basis_aux₂ α β 𝔖 h' hb)

Premises used: UniformOnFun.gen, Filter.hasBasis_biInf_of_directed, Function.comp, UniformOnFun.hasBasis_uniformity_of_basis_aux₁, UniformOnFun.hasBasis_uniformity_of_basis_aux₂
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
h : 𝔖.Nonempty
h' : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
⊢ HasBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (𝓤 (α →ᵤ[𝔖] β))
    (fun (SV : Prod.{u_1, u_2} (Set α) (Set (β × β))) ↦ SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓤 β)
    fun (SV : Prod.{u_1, u_2} (Set α) (Set (β × β))) ↦ UniformOnFun.gen 𝔖 SV.1 SV.2

Tactic:
UniformOnFun.hasBasis_uniformity_of_basis α β 𝔖 h h' (𝓤 β).basis_sets

Premises used: uniformity, Filter.basis_sets, UniformOnFun.hasBasis_uniformity_of_basis