awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
h :
  ∀ (i : ι),
    Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
      (UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
        (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ α → δ i) i)
          ((fun (i : ι) ↦ (uniformSpace α (δ i) : UniformSpace (UniformFun.{u_1, u_5} α (δ i)))) i)))
      (uniformSpace α ((i : ι) → δ i))
⊢ Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (⨅ (i : ι),
      UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
        (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ α → δ i) i)
          ((fun (i : ι) ↦ (uniformSpace α (δ i) : UniformSpace (UniformFun.{u_1, u_5} α (δ i)))) i)))
    (⨅ (i : ι), uniformSpace α ((i : ι) → δ i))

Tactic:
refine iInf_congr fun i => ?_

Premises used: iInf_congr
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
i : ι
h :
  Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ α → δ i) i ∘ Function.swap (φ := fun (a : α) ↦ δ))
      ((fun (i : ι) ↦ (uniformSpace α (δ i) : UniformSpace (UniformFun.{u_1, u_5} α (δ i)))) i))
    (UniformSpace.comap (β := α → δ i) (fun (x : α → (i : ι) → δ i) ↦ Function.eval (β := δ) i ∘ x)
      (uniformSpace α (δ i)))
⊢ Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
      (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ α → δ i) i)
        ((fun (i : ι) ↦ (uniformSpace α (δ i) : UniformSpace (UniformFun.{u_1, u_5} α (δ i)))) i)))
    (uniformSpace α ((i : ι) → δ i))

Tactic:
rw [← UniformSpace.comap_comap, UniformFun.comap_eq]

Premises used: UniformSpace.comap_comap, UniformFun.comap_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst : UniformSpace β
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
i : ι
⊢ Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ α → δ i) i ∘ Function.swap (φ := fun (a : α) ↦ δ))
      ((fun (i : ι) ↦ (uniformSpace α (δ i) : UniformSpace (UniformFun.{u_1, u_5} α (δ i)))) i))
    (UniformSpace.comap (β := α → δ i) (fun (x : α → (i : ι) → δ i) ↦ Function.eval (β := δ) i ∘ x)
      (uniformSpace α (δ i)))

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
inst_1 : TopologicalSpace α
⊢ IsClosed[topologicalSpace α β]
    {f : α →ᵤ β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun : (a : α →ᵤ β) → α → β) f)}

Tactic:
isClosed_iff_forall_filter.2 fun f u _ hu huf ↦ ?_

Premises used: Iff.mpr, isClosed_iff_forall_filter
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
inst_1 : TopologicalSpace α
refine :
  ∀ (f : α →ᵤ β) (u : Filter (α →ᵤ β)),
    u.NeBot →
      ∀ (hu : u ≤ 𝓟 {f : α →ᵤ β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun : (a : α →ᵤ β) → α → β) f)})
        (huf : u ≤ 𝓝 f),
        Membership.mem (γ := Set (α →ᵤ β))
          {f : α →ᵤ β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun : (a : α →ᵤ β) → α → β) f)} f
⊢ IsClosed[topologicalSpace α β]
    {f : α →ᵤ β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun : (a : α →ᵤ β) → α → β) f)}

Tactic:
refine isClosed_iff_forall_filter.2 fun f u _ hu huf ↦ ?_

Premises used: Iff.mpr, isClosed_iff_forall_filter
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
inst_1 : TopologicalSpace α
f : α →ᵤ β
u : Filter (α →ᵤ β)
h : u.NeBot
hu : u ≤ 𝓟 {f : α →ᵤ β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun : (a : α →ᵤ β) → α → β) f)}
huf : u ≤ 𝓝 f
⊢ TendstoUniformly (α := α) (β := β) ((⇑toFun : (a : α →ᵤ β) → α → β) ∘ id) ((toFun : (a : α →ᵤ β) → α → β) f) u

Tactic:
rw [← tendsto_id', UniformFun.tendsto_iff_tendstoUniformly] at huf

Premises used: UniformFun.tendsto_iff_tendstoUniformly, Filter.tendsto_id'
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
inst_1 : TopologicalSpace α
f : α →ᵤ β
u : Filter (α →ᵤ β)
h : u.NeBot
hu : u ≤ 𝓟 {f : α →ᵤ β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun : (a : α →ᵤ β) → α → β) f)}
huf : TendstoUniformly (α := α) (β := β) ((⇑toFun : (a : α →ᵤ β) → α → β) ∘ id) ((toFun : (a : α →ᵤ β) → α → β) f) u
⊢ Membership.mem (γ := Set (α →ᵤ β))
    {f : α →ᵤ β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun : (a : α →ᵤ β) → α → β) f)} f

Tactic:
huf.continuous <| Eventually.frequently (le_principal_iff.mp hu)

Premises used: Filter.le_principal_iff, Set.Mem, setOf, Filter.Eventually.frequently, Iff.mp, TendstoUniformly.continuous
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
inst_1 : TopologicalSpace α
f : α →ᵤ β
u : Filter (α →ᵤ β)
h : u.NeBot
hu : u ≤ 𝓟 {f : α →ᵤ β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun : (a : α →ᵤ β) → α → β) f)}
huf : TendstoUniformly (α := α) (β := β) ((⇑toFun : (a : α →ᵤ β) → α → β) ∘ id) ((toFun : (a : α →ᵤ β) → α → β) f) u
⊢ Membership.mem (γ := Set (α →ᵤ β))
    {f : α →ᵤ β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun : (a : α →ᵤ β) → α → β) f)} f

Tactic:
exact huf.continuous <| Eventually.frequently (le_principal_iff.mp hu)

Premises used: Filter.le_principal_iff, Filter.Eventually.frequently, Iff.mp, TendstoUniformly.continuous
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
h : Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))
⊢ uniformSpace α β =
    UniformSpace.comap
        (Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
          ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
        (uniformSpace δ₁ β) ⊓
      UniformSpace.comap
        (Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
          ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
        (uniformSpace δ₂ β)

Tactic:
ext : 1
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))

Tactic:
le_antisymm (le_inf ?_ ?_) ?_

Premises used: le_inf, le_antisymm
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
h : LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))
h₁ : LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))
h₂ : LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))
⊢ Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))

Tactic:
refine le_antisymm (le_inf ?_ ?_) ?_

Premises used: le_inf, le_antisymm
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))

Tactic:
tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous

Premises used: Set.Mem, Filter.tendsto_iff_comap, UniformFun.precomp_uniformContinuous, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))

Tactic:
exact tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous

Premises used: Filter.tendsto_iff_comap, UniformFun.precomp_uniformContinuous, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
⊢ LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))

Tactic:
(UniformFun.hasBasis_uniformity δ₁ β |>.comap _).inf
      (UniformFun.hasBasis_uniformity δ₂ β |>.comap _)
        |>.le_basis_iff (UniformFun.hasBasis_uniformity α β) |>.mpr fun U hU ↦
        ⟨⟨U, U⟩, ⟨hU, hU⟩, fun ⟨f, g⟩ hfg x ↦ ?_⟩

Premises used: Iff.mpr, Filter.HasBasis.inf, Set.Mem, UniformFun.hasBasis_uniformity, setOf, Membership.mem, Filter.HasBasis.le_basis_iff, Prod.mk, UniformFun.toFun, Prod.fst, Filter.HasBasis.comap, And.intro, Exists.intro, _private.0.UniformFun.uniformSpace_eq_inf_precomp_of_cover.match_1, Prod.snd, DFunLike.coe
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
h :
  ∀ (U : Set (β × β)) (hU : U ∈ 𝓤 β) (x : (α →ᵤ β) × (α →ᵤ β)) (x : α) (f g : α →ᵤ β)
    (hfg :
      Membership.mem (γ := Set ((α →ᵤ β) × (α →ᵤ β)))
        ((fun (p : (α →ᵤ β) × (α →ᵤ β)) ↦
              (Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
                  ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.1,
                Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
                  ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.2)) ⁻¹'
            UniformFun.gen δ₁ β (U, U).1 ∩
          (fun (p : (α →ᵤ β) × (α →ᵤ β)) ↦
              (Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
                  ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.1,
                Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
                  ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.2)) ⁻¹'
            UniformFun.gen δ₂ β (U, U).2)
        (f, g)),
    Membership.mem (α := β × β) U
      (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 x, (toFun : (a : α →ᵤ β) → α → β) (f, g).2 x) : β × β)
⊢ LE.le (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))

Tactic:
refine
      (UniformFun.hasBasis_uniformity δ₁ β |>.comap _).inf
      (UniformFun.hasBasis_uniformity δ₂ β |>.comap _)
        |>.le_basis_iff (UniformFun.hasBasis_uniformity α β) |>.mpr fun U hU ↦
        ⟨⟨U, U⟩, ⟨hU, hU⟩, fun ⟨f, g⟩ hfg x ↦ ?_⟩

Premises used: Iff.mpr, Filter.HasBasis.inf, UniformFun.hasBasis_uniformity, Filter.HasBasis.le_basis_iff, Prod.mk, Filter.HasBasis.comap, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x_1 : (α →ᵤ β) × (α →ᵤ β)
x : α
f g : α →ᵤ β
hfg :
  Membership.mem (γ := Set ((α →ᵤ β) × (α →ᵤ β)))
    ((fun (p : (α →ᵤ β) × (α →ᵤ β)) ↦
          (Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.1,
            Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.2)) ⁻¹'
        UniformFun.gen δ₁ β (U, U).1 ∩
      (fun (p : (α →ᵤ β) × (α →ᵤ β)) ↦
          (Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.1,
            Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.2)) ⁻¹'
        UniformFun.gen δ₂ β (U, U).2)
    (f, g)
h :
  ∀ (y : δ₁),
    Membership.mem (α := β × β) U
      (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 (φ₁ y), (toFun : (a : α →ᵤ β) → α → β) (f, g).2 (φ₁ y)) : β × β)
h₁ :
  ∀ (y : δ₂),
    Membership.mem (α := β × β) U
      (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 (φ₂ y), (toFun : (a : α →ᵤ β) → α → β) (f, g).2 (φ₂ y)) : β × β)
⊢ Membership.mem (α := β × β) U
    (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 x, (toFun : (a : α →ᵤ β) → α → β) (f, g).2 x) : β × β)

Tactic:
rcases h_cover.ge <| mem_univ x with (⟨y, rfl⟩ | ⟨y, rfl⟩)

Premises used: Eq.ge, Set.mem_univ, rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x : (α →ᵤ β) × (α →ᵤ β)
f g : α →ᵤ β
hfg :
  Membership.mem (γ := Set ((α →ᵤ β) × (α →ᵤ β)))
    ((fun (p : (α →ᵤ β) × (α →ᵤ β)) ↦
          (Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.1,
            Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.2)) ⁻¹'
        UniformFun.gen δ₁ β (U, U).1 ∩
      (fun (p : (α →ᵤ β) × (α →ᵤ β)) ↦
          (Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.1,
            Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.2)) ⁻¹'
        UniformFun.gen δ₂ β (U, U).2)
    (f, g)
y : δ₁
⊢ Membership.mem (α := β × β) U
    (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 (φ₁ y), (toFun : (a : α →ᵤ β) → α → β) (f, g).2 (φ₁ y)) : β × β)

Tactic:
hfg.1 y

Premises used: Set.Mem, And.left
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x : (α →ᵤ β) × (α →ᵤ β)
f g : α →ᵤ β
hfg :
  Membership.mem (γ := Set ((α →ᵤ β) × (α →ᵤ β)))
    ((fun (p : (α →ᵤ β) × (α →ᵤ β)) ↦
          (Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.1,
            Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.2)) ⁻¹'
        UniformFun.gen δ₁ β (U, U).1 ∩
      (fun (p : (α →ᵤ β) × (α →ᵤ β)) ↦
          (Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.1,
            Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.2)) ⁻¹'
        UniformFun.gen δ₂ β (U, U).2)
    (f, g)
y : δ₁
⊢ Membership.mem (α := β × β) U
    (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 (φ₁ y), (toFun : (a : α →ᵤ β) → α → β) (f, g).2 (φ₁ y)) : β × β)

Tactic:
exact hfg.1 y

Premises used: And.left
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x : (α →ᵤ β) × (α →ᵤ β)
f g : α →ᵤ β
hfg :
  Membership.mem (γ := Set ((α →ᵤ β) × (α →ᵤ β)))
    ((fun (p : (α →ᵤ β) × (α →ᵤ β)) ↦
          (Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.1,
            Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.2)) ⁻¹'
        UniformFun.gen δ₁ β (U, U).1 ∩
      (fun (p : (α →ᵤ β) × (α →ᵤ β)) ↦
          (Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.1,
            Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.2)) ⁻¹'
        UniformFun.gen δ₂ β (U, U).2)
    (f, g)
y : δ₂
⊢ Membership.mem (α := β × β) U
    (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 (φ₂ y), (toFun : (a : α →ᵤ β) → α → β) (f, g).2 (φ₂ y)) : β × β)

Tactic:
hfg.2 y

Premises used: Set.Mem, And.right
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
δ₁ : Type u_6
δ₂ : Type u_7
φ₁ : δ₁ → α
φ₂ : δ₂ → α
h_cover : range φ₁ ∪ range φ₂ = univ
U : Set (β × β)
hU : U ∈ 𝓤 β
x : (α →ᵤ β) × (α →ᵤ β)
f g : α →ᵤ β
hfg :
  Membership.mem (γ := Set ((α →ᵤ β) × (α →ᵤ β)))
    ((fun (p : (α →ᵤ β) × (α →ᵤ β)) ↦
          (Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.1,
            Function.comp (β := δ₁ → β) (⇑ofFun : (a : δ₁ → β) → δ₁ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.2)) ⁻¹'
        UniformFun.gen δ₁ β (U, U).1 ∩
      (fun (p : (α →ᵤ β) × (α →ᵤ β)) ↦
          (Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.1,
            Function.comp (β := δ₂ → β) (⇑ofFun : (a : δ₂ → β) → δ₂ →ᵤ β)
              ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)) p.2)) ⁻¹'
        UniformFun.gen δ₂ β (U, U).2)
    (f, g)
y : δ₂
⊢ Membership.mem (α := β × β) U
    (((toFun : (a : α →ᵤ β) → α → β) (f, g).1 (φ₂ y), (toFun : (a : α →ᵤ β) → α → β) (f, g).2 (φ₂ y)) : β × β)

Tactic:
exact hfg.2 y

Premises used: And.right
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ (I : Set ι), I.Finite ∧ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, range (φ i)) univ
h : Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))
⊢ uniformSpace α β =
    ⨅ (i : ι),
      UniformSpace.comap (β := UniformFun.{u_6, u_2} (δ i) β)
        (Function.comp (β := δ i → β) (⇑ofFun : (a : δ i → β) → δ i →ᵤ β)
          ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑toFun : (a : α →ᵤ β) → α → β)))
        (uniformSpace (δ i) β)

Tactic:
ext : 1
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ (I : Set ι), I.Finite ∧ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, range (φ i)) univ
h :
  Eq (α := 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) β)))
⊢ Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β)) (𝓤 (α →ᵤ β))

Tactic:
simp_rw [iInf_uniformity, uniformity_comap]

Premises used: iInf_uniformity, uniformity_comap
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ (I : Set ι), I.Finite ∧ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, range (φ i)) univ
⊢ Eq (α := 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:
le_antisymm (le_iInf fun i ↦ tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous) ?_

Premises used: le_iInf, Filter.tendsto_iff_comap, UniformFun.precomp_uniformContinuous, le_antisymm, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ (I : Set ι), I.Finite ∧ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, range (φ i)) univ
h :
  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) β)))
    (𝓤 (α →ᵤ β))
⊢ Eq (α := 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 le_antisymm (le_iInf fun i ↦ tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous) ?_

Premises used: le_iInf, Filter.tendsto_iff_comap, UniformFun.precomp_uniformContinuous, le_antisymm, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ (I : Set ι), I.Finite ∧ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ I, range (φ i)) univ
h :
  ∀ (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) β)))
      (𝓤 (α →ᵤ β))
⊢ 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:
rcases h_cover with ⟨I, I_finite, I_cover⟩