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
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : CompleteSpace β
inl : IsEmpty β → CompleteSpace (α →ᵤ[𝔖] β)
inr : Nonempty β → CompleteSpace (α →ᵤ[𝔖] β)
⊢ CompleteSpace (α →ᵤ[𝔖] β)

Tactic:
rcases isEmpty_or_nonempty β

Premises used: isEmpty_or_nonempty
-- 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 α)
inst_1 : CompleteSpace β
h : IsEmpty β
⊢ CompleteSpace (α →ᵤ[𝔖] β)

Tactic:
infer_instance
-- 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 α)
inst_1 : CompleteSpace β
h : Nonempty β
⊢ CompleteSpace (α →ᵤ[𝔖] β)

Tactic:
⟨fun {F} hF ↦ ?_⟩

Premises used: CompleteSpace.mk
-- 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 α)
inst_1 : CompleteSpace β
h : Nonempty β
inr : ∀ {F : Filter (α →ᵤ[𝔖] β)} (hF : Cauchy F), ∃ (x : α →ᵤ[𝔖] β), F ≤ 𝓝 x
⊢ CompleteSpace (α →ᵤ[𝔖] β)

Tactic:
refine ⟨fun {F} hF ↦ ?_⟩
-- 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 α)
inst_1 : CompleteSpace β
h : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
⊢ F.NeBot

Tactic:
have := hF.1
-- 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 α)
inst_1 : CompleteSpace β
h : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
⊢ ∀ x ∈ ⋃₀ 𝔖, ∃ (y : β), Tendsto (fun (x_1 : α →ᵤ[𝔖] β) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_1 x) F (𝓝 y)

Tactic:
have : ∀ x ∈ ⋃₀ 𝔖, ∃ y : β, Tendsto (toFun 𝔖 · x) F (𝓝 y) := fun x hx ↦
      CompleteSpace.complete (hF.map (uniformContinuous_eval_of_mem_sUnion _ _ hx))
-- 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 α)
inst_1 : CompleteSpace β
h : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this_1 : F.NeBot
this : ∀ x ∈ ⋃₀ 𝔖, ∃ (y : β), Tendsto (fun (x_1 : α →ᵤ[𝔖] β) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_1 x) F (𝓝 y)
inr :
  ∀ (g : (x : α) → β)
    (hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun (x_1 : α →ᵤ[𝔖] β) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_1 x) F (𝓝 (g x))),
    ∃ (x : α →ᵤ[𝔖] β), F ≤ 𝓝 x
⊢ ∃ (x : α →ᵤ[𝔖] β), F ≤ 𝓝 x

Tactic:
choose! g hg using this
-- 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 α)
inst_1 : CompleteSpace β
h_1 : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : (x : α) → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun (x_1 : α →ᵤ[𝔖] β) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_1 x) F (𝓝 (g x))
h : F ≤ 𝓝 ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) g)
⊢ ∃ (x : α →ᵤ[𝔖] β), F ≤ 𝓝 x

Tactic:
use ofFun 𝔖 g

Premises used: UniformOnFun.ofFun, DFunLike.coe
-- 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 α)
inst_1 : CompleteSpace β
h_1 : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : (x : α) → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun (x_1 : α →ᵤ[𝔖] β) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_1 x) F (𝓝 (g x))
h :
  ∀ (i : Set α) (j : i ∈ 𝔖) (i_1 : SetRel β β) (j : i_1 ∈ 𝓤 β ∧ IsClosed[instTopologicalSpaceProd] i_1),
    {g_1 : α →ᵤ[𝔖] β |
        ∀ x ∈ i,
          Membership.mem (α := β × β) (id i_1)
            (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) g : α →ᵤ[𝔖] β) x,
                (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g_1 x) :
              β × β)} ∈
      F
⊢ F ≤ 𝓝 ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) g)

Tactic:
simp_rw [UniformOnFun.nhds_eq_of_basis _ _ uniformity_hasBasis_closed, le_iInf₂_iff,
      le_principal_iff]

Premises used: uniformity_hasBasis_closed, Filter.le_principal_iff, UniformOnFun.nhds_eq_of_basis, le_iInf₂_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s_1 : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : CompleteSpace β
h_1 : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : (x : α) → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun (x_1 : α →ᵤ[𝔖] β) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_1 x) F (𝓝 (g x))
s : Set α
hs : s ∈ 𝔖
U : SetRel β β
h :
  ∀ (hU : U ∈ 𝓤 β) (hUc : IsClosed[instTopologicalSpaceProd] U),
    {g_1 : α →ᵤ[𝔖] β |
        ∀ x ∈ s,
          Membership.mem (α := β × β) (id U)
            (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) g : α →ᵤ[𝔖] β) x,
                (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g_1 x) :
              β × β)} ∈
      F
⊢ ∀ (j : U ∈ 𝓤 β ∧ IsClosed[instTopologicalSpaceProd] U),
    {g_1 : α →ᵤ[𝔖] β |
        ∀ x ∈ s,
          Membership.mem (α := β × β) (id U)
            (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) g : α →ᵤ[𝔖] β) x,
                (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g_1 x) :
              β × β)} ∈
      F

Tactic:
⟨hU, hUc⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s_1 : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : CompleteSpace β
h_1 : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : (x : α) → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun (x_1 : α →ᵤ[𝔖] β) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_1 x) F (𝓝 (g x))
s : Set α
hs : s ∈ 𝔖
U : SetRel β β
hU : U ∈ 𝓤 β
hUc : IsClosed[instTopologicalSpaceProd] U
h :
  ∀ (V : Set (α →ᵤ[𝔖] β)) (hV : V ∈ F) (hVU : V ×ˢ V ⊆ UniformOnFun.gen 𝔖 s U),
    {g_1 : α →ᵤ[𝔖] β |
        ∀ x ∈ s,
          Membership.mem (α := β × β) (id U)
            (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) g : α →ᵤ[𝔖] β) x,
                (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g_1 x) :
              β × β)} ∈
      F
⊢ {g_1 : α →ᵤ[𝔖] β |
      ∀ x ∈ s,
        Membership.mem (α := β × β) (id U)
          (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) g : α →ᵤ[𝔖] β) x,
              (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g_1 x) :
            β × β)} ∈
    F

Tactic:
rcases cauchy_iff.mp hF |>.2 _ <| UniformOnFun.gen_mem_uniformity _ _ hs hU
      with ⟨V, hV, hVU⟩

Premises used: cauchy_iff, And.right, UniformOnFun.gen_mem_uniformity, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s_1 : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : CompleteSpace β
h_1 : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : (x : α) → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun (x_1 : α →ᵤ[𝔖] β) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_1 x) F (𝓝 (g x))
s : Set α
hs : s ∈ 𝔖
U : SetRel β β
hU : U ∈ 𝓤 β
hUc : IsClosed[instTopologicalSpaceProd] U
V : Set (α →ᵤ[𝔖] β)
hV : V ∈ F
hVU : V ×ˢ V ⊆ UniformOnFun.gen 𝔖 s U
h :
  ∀ (f : α →ᵤ[𝔖] β) (hf : f ∈ V) (x : α) (hx : x ∈ s),
    Membership.mem (α := β × β) (id U)
      (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) g : α →ᵤ[𝔖] β) x,
          (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) :
        β × β)
⊢ {g_1 : α →ᵤ[𝔖] β |
      ∀ x ∈ s,
        Membership.mem (α := β × β) (id U)
          (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) g : α →ᵤ[𝔖] β) x,
              (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g_1 x) :
            β × β)} ∈
    F

Tactic:
filter_upwards [hV] with f hf x hx
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s_1 : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : CompleteSpace β
h : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : (x : α) → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun (x_1 : α →ᵤ[𝔖] β) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_1 x) F (𝓝 (g x))
s : Set α
hs : s ∈ 𝔖
U : SetRel β β
hU : U ∈ 𝓤 β
hUc : IsClosed[instTopologicalSpaceProd] U
V : Set (α →ᵤ[𝔖] β)
hV : V ∈ F
hVU : V ×ˢ V ⊆ UniformOnFun.gen 𝔖 s U
f : α →ᵤ[𝔖] β
hf : f ∈ V
x : α
hx : x ∈ s
⊢ Membership.mem (α := β × β) (id U)
    (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) g : α →ᵤ[𝔖] β) x,
        (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) :
      β × β)

Tactic:
hUc.mem_of_tendsto ((hg x ⟨s, hs, hx⟩).prodMk_nhds tendsto_const_nhds) ?_

Premises used: Set.Mem, tendsto_const_nhds, IsClosed.mem_of_tendsto, And.intro, Exists.intro, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s_1 : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : CompleteSpace β
h_1 : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : (x : α) → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun (x_1 : α →ᵤ[𝔖] β) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_1 x) F (𝓝 (g x))
s : Set α
hs : s ∈ 𝔖
U : SetRel β β
hU : U ∈ 𝓤 β
hUc : IsClosed[instTopologicalSpaceProd] U
V : Set (α →ᵤ[𝔖] β)
hV : V ∈ F
hVU : V ×ˢ V ⊆ UniformOnFun.gen 𝔖 s U
f : α →ᵤ[𝔖] β
hf : f ∈ V
x : α
hx : x ∈ s
h :
  ∀ᶠ (x_1 : α →ᵤ[𝔖] β) in F,
    Membership.mem (α := β × β) U
      (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_1 x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) : β × β)
⊢ Membership.mem (α := β × β) (id U)
    (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) g : α →ᵤ[𝔖] β) x,
        (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) :
      β × β)

Tactic:
refine hUc.mem_of_tendsto ((hg x ⟨s, hs, hx⟩).prodMk_nhds tendsto_const_nhds) ?_

Premises used: tendsto_const_nhds, IsClosed.mem_of_tendsto, And.intro, Exists.intro, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s_1 : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : CompleteSpace β
h : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : (x : α) → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun (x_1 : α →ᵤ[𝔖] β) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_1 x) F (𝓝 (g x))
s : Set α
hs : s ∈ 𝔖
U : SetRel β β
hU : U ∈ 𝓤 β
hUc : IsClosed[instTopologicalSpaceProd] U
V : Set (α →ᵤ[𝔖] β)
hV : V ∈ F
hVU : V ×ˢ V ⊆ UniformOnFun.gen 𝔖 s U
f : α →ᵤ[𝔖] β
hf : f ∈ V
x : α
hx : x ∈ s
g' : α →ᵤ[𝔖] β
hg' : g' ∈ V
⊢ Membership.mem (α := β × β) U
    (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g' x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) : β × β)

Tactic:
hVU (mk_mem_prod hg' hf) _ hx

Premises used: Set.Mem, Set.mk_mem_prod
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s_1 : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : CompleteSpace β
h_1 : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : (x : α) → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun (x_1 : α →ᵤ[𝔖] β) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_1 x) F (𝓝 (g x))
s : Set α
hs : s ∈ 𝔖
U : SetRel β β
hU : U ∈ 𝓤 β
hUc : IsClosed[instTopologicalSpaceProd] U
V : Set (α →ᵤ[𝔖] β)
hV : V ∈ F
hVU : V ×ˢ V ⊆ UniformOnFun.gen 𝔖 s U
f : α →ᵤ[𝔖] β
hf : f ∈ V
x : α
hx : x ∈ s
h :
  ∀ (a : α →ᵤ[𝔖] β),
    Membership.mem (γ := Set (α →ᵤ[𝔖] β))
      {x_1 : α →ᵤ[𝔖] β |
        x_1 ∈ V →
          Membership.mem (γ := Set (α →ᵤ[𝔖] β))
            {x_2 : α →ᵤ[𝔖] β |
              (fun (x_3 : α →ᵤ[𝔖] β) ↦
                  Membership.mem (α := β × β) U
                    (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_3 x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) : β × β))
                x_2}
            x_1}
      a
h₁ h₂ :
  ∀ (g' : α →ᵤ[𝔖] β) (hg' : g' ∈ V),
    Membership.mem (α := β × β) U
      (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g' x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) : β × β)
⊢ ∀ᶠ (x_1 : α →ᵤ[𝔖] β) in F,
    Membership.mem (α := β × β) U
      (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_1 x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) : β × β)

Tactic:
filter_upwards [hV] with g' hg' using hVU (mk_mem_prod hg' hf) _ hx
-- 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 α)
inst_1 : UniformSpace γ
comap_uniformity :
  Eq (α := Filter ((α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ)))
    (comap (β := ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)) × (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
      (fun (x : (α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ)) ↦
        ((Equiv.trans (Equiv.symm (ofFun 𝔖))
                (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                  (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
              (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
            x.1,
          (Equiv.trans (Equiv.symm (ofFun 𝔖))
                (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                  (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
              (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
            x.2))
      (𝓤 ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))))
    (𝓤 (α →ᵤ[𝔖] β × γ))
⊢ IsUniformInducing (α := α →ᵤ[𝔖] β × γ) (β := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
    (⇑(Equiv.trans (Equiv.symm (ofFun 𝔖))
          (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
            (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖)))) :
      (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))

Tactic:
constructor
-- 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 α)
inst_1 : UniformSpace γ
comap_uniformity :
  Eq (α := Filter ((α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ)))
    (comap (β := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
        ((fun (p : ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)) × (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)) ↦ (p.1.1, p.2.1)) ∘
          fun (x : (α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ)) ↦
          ((Equiv.trans (Equiv.symm (ofFun 𝔖))
                  (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                    (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
                (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
              x.1,
            (Equiv.trans (Equiv.symm (ofFun 𝔖))
                  (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                    (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
                (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap (β := (α →ᵤ[𝔖] γ) × (α →ᵤ[𝔖] γ))
        ((fun (p : ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)) × (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)) ↦ (p.1.2, p.2.2)) ∘
          fun (x : (α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ)) ↦
          ((Equiv.trans (Equiv.symm (ofFun 𝔖))
                  (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                    (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
                (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
              x.1,
            (Equiv.trans (Equiv.symm (ofFun 𝔖))
                  (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                    (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
                (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
              x.2))
        (𝓤 (α →ᵤ[𝔖] γ)))
    (𝓤 (α →ᵤ[𝔖] β × γ))
⊢ Eq (α := Filter ((α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ)))
    (comap (β := ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)) × (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
      (fun (x : (α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ)) ↦
        ((Equiv.trans (Equiv.symm (ofFun 𝔖))
                (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                  (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
              (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
            x.1,
          (Equiv.trans (Equiv.symm (ofFun 𝔖))
                (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                  (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
              (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
            x.2))
      (𝓤 ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))))
    (𝓤 (α →ᵤ[𝔖] β × γ))

Tactic:
rw [uniformity_prod, comap_inf, comap_comap, comap_comap]

Premises used: Filter.comap_inf, Filter.comap_comap, uniformity_prod
-- 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 α)
inst_1 : UniformSpace γ
⊢ Eq (α := UniformSpace (α →ᵤ[𝔖] β × γ)) (uniformSpace α (β × γ) 𝔖)
    (uniformSpace α (β × γ) 𝔖 ⊓ uniformSpace α (β × γ) 𝔖)

Tactic:
have H := @UniformOnFun.inf_eq α (β × γ) 𝔖
        (UniformSpace.comap Prod.fst ‹_›) (UniformSpace.comap Prod.snd ‹_›)
-- 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 α)
inst_1 : UniformSpace γ
H :
  Eq (α := UniformSpace (α →ᵤ[𝔖] β × γ)) (uniformSpace α (β × γ) 𝔖)
    (uniformSpace α (β × γ) 𝔖 ⊓ uniformSpace α (β × γ) 𝔖)
⊢ Eq (α := Filter ((α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ))) (𝓤 (α →ᵤ[𝔖] β × γ)) (𝓤 (α →ᵤ[𝔖] β × γ))

Tactic:
apply_fun (fun u ↦ @uniformity (α →ᵤ[𝔖] β × γ) u) at H

Premises used: uniformity, UniformOnFun, Prod
-- 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 α)
inst_1 : UniformSpace γ
H : Eq (α := Filter ((α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ))) (𝓤 (α →ᵤ[𝔖] β × γ)) (𝓤 (α →ᵤ[𝔖] β × γ))
⊢ Eq (α := Filter ((α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ))) (𝓤 (α →ᵤ[𝔖] β × γ)) (𝓤 (α →ᵤ[𝔖] β × γ))

Tactic:
H.symm

Premises used: Eq.symm
-- 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 α)
inst_1 : UniformSpace γ
H : Eq (α := Filter ((α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ))) (𝓤 (α →ᵤ[𝔖] β × γ)) (𝓤 (α →ᵤ[𝔖] β × γ))
⊢ Eq (α := Filter ((α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ)))
    (comap (β := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
        ((fun (p : ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)) × (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)) ↦ (p.1.1, p.2.1)) ∘
          fun (x : (α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ)) ↦
          ((Equiv.trans (Equiv.symm (ofFun 𝔖))
                  (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                    (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
                (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
              x.1,
            (Equiv.trans (Equiv.symm (ofFun 𝔖))
                  (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                    (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
                (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap (β := (α →ᵤ[𝔖] γ) × (α →ᵤ[𝔖] γ))
        ((fun (p : ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)) × (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)) ↦ (p.1.2, p.2.2)) ∘
          fun (x : (α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ)) ↦
          ((Equiv.trans (Equiv.symm (ofFun 𝔖))
                  (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                    (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
                (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
              x.1,
            (Equiv.trans (Equiv.symm (ofFun 𝔖))
                  (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
                    (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))) :
                (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
              x.2))
        (𝓤 (α →ᵤ[𝔖] γ)))
    (comap (β := (α → β) × (α → β)) (Prod.map (fun (x : α → β × γ) ↦ Prod.fst ∘ x) fun (x : α → β × γ) ↦ Prod.fst ∘ x)
        (𝓤 (α → β)) ⊓
      comap (β := (α → γ) × (α → γ)) (Prod.map (fun (x : α → β × γ) ↦ Prod.snd ∘ x) fun (x : α → β × γ) ↦ Prod.snd ∘ x)
        (𝓤 (α → γ)))

Tactic:
rfl
-- 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 α)
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
comap_uniformity :
  Eq (α := Filter ((α →ᵤ[𝔖] (i : ι) → δ i) × (α →ᵤ[𝔖] (i : ι) → δ i)))
    (comap (β := ((i : ι) → UniformOnFun.{u_1, u_5} α (δ i) 𝔖) × ((i : ι) → UniformOnFun.{u_1, u_5} α (δ i) 𝔖))
      (fun (x : (α →ᵤ[𝔖] (i : ι) → δ i) × (α →ᵤ[𝔖] (i : ι) → δ i)) ↦
        ((Equiv.piComm fun (a : α) ↦ δ : (a : α →ᵤ[𝔖] (i : ι) → δ i) → (i : ι) → α →ᵤ[𝔖] δ i) x.1,
          (Equiv.piComm fun (a : α) ↦ δ : (a : α →ᵤ[𝔖] (i : ι) → δ i) → (i : ι) → α →ᵤ[𝔖] δ i) x.2))
      (𝓤 ((i : ι) → UniformOnFun.{u_1, u_5} α (δ i) 𝔖)))
    (𝓤 (α →ᵤ[𝔖] (i : ι) → δ i))
⊢ IsUniformInducing (α := α →ᵤ[𝔖] (i : ι) → δ i) (β := (i : ι) → UniformOnFun.{u_1, u_5} α (δ i) 𝔖)
    (⇑(Equiv.piComm fun (a : α) ↦ δ) : (a : α →ᵤ[𝔖] (i : ι) → δ i) → (i : ι) → α →ᵤ[𝔖] δ i)

Tactic:
constructor
-- 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 α)
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
comap_uniformity :
  Eq (α := Filter (((x : α) → (y : ι) → δ y) × ((x : α) → (y : ι) → δ y)))
    (comap (Prod.map (Function.swap (φ := fun (a : α) ↦ δ)) (Function.swap (φ := fun (a : α) ↦ δ)))
      (𝓤 ((i : ι) → UniformOnFun.{u_1, u_5} α (δ i) 𝔖)))
    (𝓤 (α →ᵤ[𝔖] (i : ι) → δ i))
⊢ Eq (α := Filter ((α →ᵤ[𝔖] (i : ι) → δ i) × (α →ᵤ[𝔖] (i : ι) → δ i)))
    (comap (β := ((i : ι) → UniformOnFun.{u_1, u_5} α (δ i) 𝔖) × ((i : ι) → UniformOnFun.{u_1, u_5} α (δ i) 𝔖))
      (fun (x : (α →ᵤ[𝔖] (i : ι) → δ i) × (α →ᵤ[𝔖] (i : ι) → δ i)) ↦
        ((Equiv.piComm fun (a : α) ↦ δ : (a : α →ᵤ[𝔖] (i : ι) → δ i) → (i : ι) → α →ᵤ[𝔖] δ i) x.1,
          (Equiv.piComm fun (a : α) ↦ δ : (a : α →ᵤ[𝔖] (i : ι) → δ i) → (i : ι) → α →ᵤ[𝔖] δ i) x.2))
      (𝓤 ((i : ι) → UniformOnFun.{u_1, u_5} α (δ i) 𝔖)))
    (𝓤 (α →ᵤ[𝔖] (i : ι) → δ i))

Tactic:
change comap (Prod.map Function.swap Function.swap) _ = _

Premises used: Function.swap, Prod.map, Filter.comap
-- 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 α)
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
comap_uniformity :
  Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
      (Pi.uniformSpace fun (i : ι) ↦ UniformOnFun.{u_1, u_5} α (δ i) 𝔖))
    (uniformSpace α ((i : ι) → δ i) 𝔖)
⊢ Eq (α := Filter (((x : α) → (y : ι) → δ y) × ((x : α) → (y : ι) → δ y))) (𝓤 ((x : α) → (y : ι) → δ y))
    (𝓤 (α →ᵤ[𝔖] (i : ι) → δ i))

Tactic:
congr
-- 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 α)
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
comap_uniformity :
  Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (⨅ (i : ι),
      UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
        (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ UniformOnFun.{u_1, u_5} α (δ i) 𝔖) i)
          (uniformSpace α (δ i) 𝔖)))
    (⨅ (i : ι), uniformSpace α ((i : ι) → δ i) 𝔖)
⊢ Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
      (Pi.uniformSpace fun (i : ι) ↦ UniformOnFun.{u_1, u_5} α (δ i) 𝔖))
    (uniformSpace α ((i : ι) → δ i) 𝔖)

Tactic:
rw [Pi.uniformSpace, UniformSpace.ofCoreEq_toCore, Pi.uniformSpace,
      UniformSpace.ofCoreEq_toCore, UniformSpace.comap_iInf, UniformOnFun.iInf_eq]

Premises used: Pi.uniformSpace, UniformSpace.ofCoreEq_toCore, UniformSpace.comap_iInf, UniformOnFun.iInf_eq