awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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
⊢ {g_1 : α →ᵤ[𝔖] β |
      ∀ x ∈ s,
        Membership.mem (α := β × β) (id U)
          (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) g : α →ᵤ[𝔖] β) x,
              (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g_1 x) :
            β × β)} ∈
    F
have 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
Tactic: rcases cauchy_iff.mp hF |>.2 _ <| UniformOnFun.gen_mem_uniformity _ _ hs hU
      with ⟨V, hV, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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
⊢ {g_1 : α →ᵤ[𝔖] β |
      ∀ x ∈ s,
        Membership.mem (α := β × β) (id U)
          (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) g : α →ᵤ[𝔖] β) x,
              (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g_1 x) :
            β × β)} ∈
    F
have h : ∀ (f : α →ᵤ[𝔖] β) (hf : f ∈ V) (x : α) (hx : x ∈ s),
  Membership.mem (α := β × β) (id U)
    (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) g : α →ᵤ[𝔖] β) x,
        (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) :
      β × β)
Tactic: filter_upwards [hV] with f hf x hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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) :
      β × β)
have h : ∀ᶠ (x_1 : α →ᵤ[𝔖] β) in F,
  Membership.mem (α := β × β) U
    (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_1 x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) : β × β)
Tactic: refine hUc.mem_of_tendsto ((hg x ⟨s, hs, hx⟩).prodMk_nhds tendsto_const_nhds) ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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
⊢ ∀ᶠ (x_1 : α →ᵤ[𝔖] β) in F,
    Membership.mem (α := β × β) U
      (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_1 x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) : β × β)
have 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
Tactic: filter_upwards [hV] with g' hg' using hVU (mk_mem_prod hg' hf) _ hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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
⊢ ∀ᶠ (x_1 : α →ᵤ[𝔖] β) in F,
    Membership.mem (α := β × β) U
      (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_1 x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) : β × β)
have h₁ : ∀ a ∈ V,
  Membership.mem (α := β × β) U
    (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) a x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) : β × β)
Tactic: filter_upwards [hV] with g' hg' using hVU (mk_mem_prod hg' hf) _ hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : UniformSpace γ
⊢ IsUniformInducing (α := α →ᵤ[𝔖] β × γ) (β := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
    (⇑(Equiv.trans (Equiv.symm (ofFun 𝔖))
          (Equiv.trans (Equiv.arrowProdEquivProdArrow α (fun (a : α) ↦ β) fun (a : α) ↦ γ)
            (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖)))) :
      (a : α →ᵤ[𝔖] β × γ) → (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))
have 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))
    (𝓤 ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))))
  (𝓤 (α →ᵤ[𝔖] β × γ))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : UniformSpace γ
⊢ 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))
      (𝓤 ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))))
    (𝓤 (α →ᵤ[𝔖] β × γ))
have 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))
      (𝓤 (α →ᵤ[𝔖] γ)))
  (𝓤 (α →ᵤ[𝔖] β × γ))
Tactic: rw [uniformity_prod, comap_inf, comap_comap, comap_comap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (hypothesis)
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 (α := 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))
        (𝓤 (α →ᵤ[𝔖] γ)))
    (𝓤 (α →ᵤ[𝔖] β × γ))
have H : Eq (α := UniformSpace (α →ᵤ[𝔖] β × γ)) (uniformSpace α (β × γ) 𝔖) (uniformSpace α (β × γ) 𝔖 ⊓ uniformSpace α (β × γ) 𝔖)
Tactic: have H := @UniformOnFun.inf_eq α (β × γ) 𝔖
        (UniformSpace.comap Prod.fst ‹_›) (UniformSpace.comap Prod.snd ‹_›)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (hypothesis)
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 ((α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ)))
    (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))
        (𝓤 (α →ᵤ[𝔖] γ)))
    (𝓤 (α →ᵤ[𝔖] β × γ))
have H₁ : Eq (α := Filter ((α →ᵤ[𝔖] β × γ) × (α →ᵤ[𝔖] β × γ))) (𝓤 (α →ᵤ[𝔖] β × γ)) (𝓤 (α →ᵤ[𝔖] β × γ))
Tactic: apply_fun (fun u ↦ @uniformity (α →ᵤ[𝔖] β × γ) u) at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
⊢ IsUniformInducing (α := α →ᵤ[𝔖] (i : ι) → δ i) (β := (i : ι) → UniformOnFun.{u_1, u_5} α (δ i) 𝔖)
    (⇑(Equiv.piComm fun (a : α) ↦ δ) : (a : α →ᵤ[𝔖] (i : ι) → δ i) → (i : ι) → α →ᵤ[𝔖] δ i)
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ 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))
have 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))
Tactic: change comap (Prod.map Function.swap Function.swap) _ = _
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
⊢ Eq (α := Filter (((x : α) → (y : ι) → δ y) × ((x : α) → (y : ι) → δ y))) (𝓤 ((x : α) → (y : ι) → δ y))
    (𝓤 (α →ᵤ[𝔖] (i : ι) → δ i))
have 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) 𝔖)
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ 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) 𝔖)
have 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) 𝔖)
Tactic: rw [Pi.uniformSpace, UniformSpace.ofCoreEq_toCore, Pi.uniformSpace,
      UniformSpace.ofCoreEq_toCore, UniformSpace.comap_iInf, UniformOnFun.iInf_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
⊢ 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) 𝔖)
have comap_uniformity : ∀ (i : ι),
  Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
      (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ UniformOnFun.{u_1, u_5} α (δ i) 𝔖) i)
        (uniformSpace α (δ i) 𝔖)))
    (uniformSpace α ((i : ι) → δ i) 𝔖)
Tactic: refine iInf_congr fun i => ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
i : ι
⊢ Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
      (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ UniformOnFun.{u_1, u_5} α (δ i) 𝔖) i)
        (uniformSpace α (δ i) 𝔖)))
    (uniformSpace α ((i : ι) → δ i) 𝔖)
have comap_uniformity : Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
  (UniformSpace.comap
      (Function.eval (β := fun (i : ι) ↦ UniformOnFun.{u_1, u_5} α (δ i) 𝔖) i ∘ Function.swap (φ := fun (a : α) ↦ δ))
      (uniformSpace α (δ i) 𝔖) :
    UniformSpace ((x : α) → (y : ι) → δ y))
  (UniformSpace.comap (β := α → δ i) (fun (x : α → (i : ι) → δ i) ↦ Function.eval (β := δ) i ∘ x)
      (uniformSpace α (δ i) 𝔖) :
    UniformSpace (α → (i : ι) → δ i))
Tactic: rw [← UniformSpace.comap_comap, UniformOnFun.comap_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : TopologicalSpace α
h : IsCoherentWith 𝔖
⊢ IsClosed[topologicalSpace α β 𝔖]
    {f : α →ᵤ[𝔖] β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)}
have refine : ∀ (f : α →ᵤ[𝔖] β) (u : Filter (α →ᵤ[𝔖] β)),
  u.NeBot →
    ∀ (hu : u ≤ 𝓟 {f : α →ᵤ[𝔖] β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)})
      (huf : u ≤ 𝓝 f) (s : Set α) (hs : s ∈ 𝔖),
      ContinuousOn.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) s
Tactic: refine isClosed_iff_forall_filter.2 fun f u _ hu huf ↦ h.continuous_iff.2 fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : TopologicalSpace α
h : IsCoherentWith 𝔖
f : α →ᵤ[𝔖] β
u : Filter (α →ᵤ[𝔖] β)
h_1 : u.NeBot
hu : u ≤ 𝓟 {f : α →ᵤ[𝔖] β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)}
huf : u ≤ 𝓝 f
s : Set α
hs : s ∈ 𝔖
⊢ ContinuousOn.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) s
have rw : ∀
  (huf :
    ∀ s ∈ 𝔖,
      TendstoUniformlyOn (β := β) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ id) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)
        u s)
  (s : Set α) (hs : s ∈ 𝔖), ContinuousOn.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) s
Tactic: rw [← tendsto_id', UniformOnFun.tendsto_iff_tendstoUniformlyOn] at huf
Cleared hypotheses: huf, s, hs
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → (↑(φ₁ ⁻¹' S) : Type u_5) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → (↑(φ₂ ⁻¹' S) : Type u_6) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₂
⊢ ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (UniformSpace.comap (β := (↑(φ₁ ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₁ S)
          (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S) : Type u_5) β) ⊓
        UniformSpace.comap (β := (↑(φ₂ ⁻¹' S) : Type u_6) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₂ S)
          (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S) : Type u_6) β))
have refine : ∀ (S : Set α) (hS : S ∈ 𝔖), range (ψ₁ S) ∪ range (ψ₂ S) = univ
Tactic: refine fun S hS ↦ UniformFun.uniformSpace_eq_inf_precomp_of_cover β _ _ ?_