awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : UniformSpace γ
f : γ → β
hf : IsUniformInducing f
⊢ Eq (α := Filter ((α →ᵤ[𝔖] γ) × (α →ᵤ[𝔖] γ)))
    (comap (β := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
      (fun (x : (α →ᵤ[𝔖] γ) × (α →ᵤ[𝔖] γ)) ↦
        (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β)
            ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ)) x.1,
          Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β)
            ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ)) x.2))
      (𝓤 (α →ᵤ[𝔖] β)))
    (𝓤 (α →ᵤ[𝔖] γ))
have hf₁ : comap (Prod.map f f) (𝓤 β) = 𝓤 γ
Tactic: replace hf : (𝓤 β).comap (Prod.map f f) = _ := hf.comap_uniformity
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : UniformSpace γ
f : γ → β
hf : comap (Prod.map f f) (𝓤 β) = 𝓤 γ
⊢ Eq (α := Filter ((α →ᵤ[𝔖] γ) × (α →ᵤ[𝔖] γ)))
    (comap (β := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))
      (Prod.map
        (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β)
          ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ)))
        (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β)
          ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ))))
      (𝓤 (α →ᵤ[𝔖] β)))
    (𝓤 (α →ᵤ[𝔖] γ))
have hf₁ : 𝓤 γ = 𝓤 γ
Tactic: rw [← uniformity_comap] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ Eq (α := Filter ((α →ᵤ[𝔖] γ) × (α →ᵤ[𝔖] γ))) (𝓤 (α →ᵤ[𝔖] γ)) (𝓤 (α →ᵤ[𝔖] γ))
have comap_uniformity : UniformSpace.comap
    (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β)
      ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ)))
    (uniformSpace α β 𝔖) =
  uniformSpace α γ 𝔖
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ UniformSpace.comap
      (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β)
        ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ)))
      (uniformSpace α β 𝔖) =
    uniformSpace α γ 𝔖
have comap_uniformity : Eq (α := UniformSpace (α →ᵤ[𝔖] γ))
  (UniformSpace.comap
    (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β)
      ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ)))
    (uniformSpace α β 𝔖))
  (UniformSpace.comap (fun (x : α → γ) ↦ f ∘ x) (uniformSpace α β 𝔖))
Tactic: rw [← UniformSpace.ext hf, UniformOnFun.comap_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : MapsTo (fun (x : Set γ) ↦ f '' x) 𝔗 𝔖
⊢ UniformContinuous (β := γ →ᵤ[𝔗] β) fun (g : α →ᵤ[𝔖] β) ↦
    (ofFun 𝔗 : (a : γ → β) → γ →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g ∘ f)
have simp_rw : ∀ (i : Set γ) (i_1 : i ∈ 𝔗) (i_2 : Set (β × β)) (i_3 : i_2 ∈ 𝓤 β),
  Tendsto
    (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
      ((ofFun 𝔗 : (a : γ → β) → γ →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1 ∘ f),
        (ofFun 𝔗 : (a : γ → β) → γ →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2 ∘ f)))
    (⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V)) (𝓟 (UniformOnFun.gen 𝔗 i i_2))
Tactic: simp_rw [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : MapsTo (fun (x : Set γ) ↦ f '' x) 𝔗 𝔖
⊢ ∀ (i : Set γ) (i_1 : i ∈ 𝔗) (i_2 : Set (β × β)) (i_3 : i_2 ∈ 𝓤 β),
    Tendsto
      (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
        ((ofFun 𝔗 : (a : γ → β) → γ →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1 ∘ f),
          (ofFun 𝔗 : (a : γ → β) → γ →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2 ∘ f)))
      (⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V)) (𝓟 (UniformOnFun.gen 𝔗 i i_2))
have refine : ∀ (t : Set γ) (ht : t ∈ 𝔗) (V : Set (β × β)) (hV : V ∈ 𝓤 β),
  Tendsto
    (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
      ((ofFun 𝔗 : (a : γ → β) → γ →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1 ∘ f),
        (ofFun 𝔗 : (a : γ → β) → γ →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2 ∘ f)))
    (𝓟 (UniformOnFun.gen 𝔖 (f '' t) V)) (𝓟 (UniformOnFun.gen 𝔗 t V))
Tactic: refine fun t ht V hV ↦ tendsto_iInf' (f '' t) <| tendsto_iInf' (hf ht) <|
    tendsto_iInf' V <| tendsto_iInf' hV ?_
-- 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 α)
𝔗 : Set (Set γ)
e : γ ≃ α
he : 𝔗 ⊆ image (⇑e : (a : γ) → α) ⁻¹' 𝔖
he' : 𝔖 ⊆ preimage (⇑e : (a : γ) → α) ⁻¹' 𝔗
s : Set α
hs : s ∈ 𝔖
⊢ (⇑e.symm : (a : α) → γ) '' s ∈ 𝔗
have rw : (⇑e : (a : γ) → α) ⁻¹' s ∈ 𝔗
Tactic: rw [Equiv.image_symm_eq_preimage]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
⊢ (fun (x y : α →ᵤ[𝔖] β) ↦
      ∃ (u : Set (α →ᵤ[𝔖] β)) (v : Set (α →ᵤ[𝔖] β)),
        IsOpen[topologicalSpace α β 𝔖] u ∧ IsOpen[topologicalSpace α β 𝔖] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v)
    f g
have obtain : ∀ (x : α) (hx : ¬f x = g x),
  ∃ (u : Set (α →ᵤ[𝔖] β)) (v : Set (α →ᵤ[𝔖] β)),
    IsOpen[topologicalSpace α β 𝔖] u ∧ IsOpen[topologicalSpace α β 𝔖] v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
Tactic: obtain ⟨x, hx⟩ := not_forall.mp (mt funext hfg)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
x : α
hx : ¬f x = g x
⊢ ∃ (u : Set (α →ᵤ[𝔖] β)) (v : Set (α →ᵤ[𝔖] β)),
    IsOpen[topologicalSpace α β 𝔖] u ∧ IsOpen[topologicalSpace α β 𝔖] v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
have obtain : ∀ (s : Set α) (hs : s ∈ 𝔖) (hxs : x ∈ s),
  ∃ (u : Set (α →ᵤ[𝔖] β)) (v : Set (α →ᵤ[𝔖] β)),
    IsOpen[topologicalSpace α β 𝔖] u ∧ IsOpen[topologicalSpace α β 𝔖] v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
Tactic: obtain ⟨s, hs, hxs⟩ : ∃ s ∈ 𝔖, x ∈ s := mem_sUnion.mp (h.symm ▸ True.intro)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
⊢ UniformContinuous (α := α →ᵤ[𝔖] β) (β := (↑(⋃₀ 𝔖) : Type u_1) → β)
    (Function.comp (β := α → β) ((⋃₀ 𝔖).restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
      (α →ᵤ[𝔖] β) → (↑(⋃₀ 𝔖) : Type u_1) → β)
have rw : ∀ (i : (↑(⋃₀ 𝔖) : Type u_1)),
  UniformContinuous (β := β) fun (x : α →ᵤ[𝔖] β) ↦
    Function.comp (β := α → β) ((⋃₀ 𝔖).restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x i
Tactic: rw [uniformContinuous_pi]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
x : α
hx : x ∈ ⋃₀ 𝔖
⊢ UniformContinuous (β := β) fun (x_1 : α →ᵤ[𝔖] β) ↦
    Function.comp (β := α → β) ((⋃₀ 𝔖).restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x_1
      (Subtype.mk (p := fun (x : α) ↦ x ∈ ⋃₀ 𝔖) x hx)
have obtain : ∀ (s : Set α) (hs : s ∈ 𝔖) (hxs : x ∈ s),
  UniformContinuous (β := β) fun (x_1 : α →ᵤ[𝔖] β) ↦
    Function.comp (β := α → β) ((⋃₀ 𝔖).restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x_1
      (Subtype.mk (p := fun (x : α) ↦ x ∈ ⋃₀ 𝔖) x hx)
Tactic: obtain ⟨s : Set α, hs : s ∈ 𝔖, hxs : x ∈ s⟩ := mem_sUnion.mpr hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
⊢ IsUniformInducing (β := (s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β)
    fun (f : α →ᵤ[𝔖] β) (s : (↑𝔖 : Type u_1)) ↦
    (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
      ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f))
have simp_rw : ⨅ (i : Set α),
    ⨅ (x : i ∈ 𝔖),
      UniformSpace.comap (β := UniformFun.{u_1, u_2} (↑i : Type u_1) β)
        (Function.comp (β := (s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β)
            (Function.eval (β := fun (s : (↑𝔖 : Type u_1)) ↦ UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β)
              (Subtype.mk (p := fun (x : Set α) ↦ x ∈ 𝔖) i sorry))
            fun (f : α →ᵤ[𝔖] β) (s : (↑𝔖 : Type u_1)) ↦
            (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
              ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)) :
          (α →ᵤ[𝔖] β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
        (UniformFun.uniformSpace (↑i : Type u_1) β : UniformSpace (UniformFun.{u_1, u_2} (↑i : Type u_1) β)) =
  uniformSpace α β 𝔖
Tactic: simp_rw [isUniformInducing_iff_uniformSpace, Pi.uniformSpace_eq, UniformSpace.comap_iInf,
    ← UniformSpace.comap_comap, iInf_subtype]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
⊢ UniformContinuous (α := α →ᵤ[𝔖] β) (β := α → β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)
have rw : ∀ (i : α), UniformContinuous (β := β) fun (x : α →ᵤ[𝔖] β) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x i
Tactic: rw [uniformContinuous_pi]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x
hc : ContinuousAt.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) x
⊢ ContinuousAt (Y := β) (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) (f, x)
have rw : ∀ s ∈ 𝓤 β,
  ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
    Membership.mem (α := β × β) (SetRel.comp s s)
      (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f, x).1 (f, x).2))
          (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) a :
        β × β)
Tactic: rw [ContinuousAt, nhds_eq_comap_uniformity, tendsto_comap_iff, ← lift'_comp_uniformity,
    tendsto_lift']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x
hc : ContinuousAt.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) x
U : Set (β × β)
hU : U ∈ 𝓤 β
⊢ ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
    Membership.mem (α := β × β) (SetRel.comp U U)
      (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f, x).1 (f, x).2))
          (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) a :
        β × β)
have rcases : ∀ (V : Set α) (hV : V ∈ 𝔖) (hVx : V ∈ 𝓝 x),
  ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
    Membership.mem (α := β × β) (SetRel.comp U U)
      (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f, x).1 (f, x).2))
          (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) a :
        β × β)
Tactic: rcases h𝔖 with ⟨V, hV, hVx⟩
Cleared hypotheses: h𝔖
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
hc : ContinuousAt.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) x
U : Set (β × β)
hU : U ∈ 𝓤 β
V : Set α
hV : V ∈ 𝔖
hVx : V ∈ 𝓝 x
g : α →ᵤ[𝔖] β
y : α
⊢ (g, y) ∈
      SProd.sprod (α := Set (α →ᵤ[𝔖] β))
        {g : α →ᵤ[𝔖] β |
          ∀ x ∈ V,
            Membership.mem (α := β × β) U
              (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
        (V ∩
          preimage.{u_1, u_2} (β := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f : α → β)
            (UniformSpace.ball ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) U : Set β)) →
    Membership.mem (α := β × β) (SetRel.comp U U)
      (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x))
          (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) (g, y) :
        β × β)
have h : ∀
  (hg :
    Membership.mem (γ := Set (α →ᵤ[𝔖] β))
      {g : α →ᵤ[𝔖] β |
        ∀ x ∈ V,
          Membership.mem (α := β × β) U
            (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
      (g, y).1)
  (hyV : (g, y).2 ∈ V)
  (hy :
    Membership.mem (γ := Set α)
      (preimage.{u_1, u_2} (β := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f : α → β)
        (UniformSpace.ball ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) U : Set β))
      (g, y).2),
  Membership.mem (α := β × β) (SetRel.comp U U)
    (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x))
        (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) (g, y) :
      β × β)
Tactic: ⟨hg, hyV, hy⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
hc : ContinuousAt.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) x
U : Set (β × β)
hU : U ∈ 𝓤 β
V : Set α
hV : V ∈ 𝔖
hVx : V ∈ 𝓝 x
⊢ ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
    Membership.mem (α := β × β) (SetRel.comp U U)
      (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f, x).1 (f, x).2))
          (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) a :
        β × β)
have h : ∀ (a : (α →ᵤ[𝔖] β) × α),
  Membership.mem (γ := Set ((α →ᵤ[𝔖] β) × α))
    {x_1 : (α →ᵤ[𝔖] β) × α |
      x_1 ∈
          SProd.sprod (α := Set (α →ᵤ[𝔖] β))
            {g : α →ᵤ[𝔖] β |
              ∀ x ∈ V,
                Membership.mem (α := β × β) U
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
            (V ∩
              preimage.{u_1, u_2} (β := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f : α → β)
                (UniformSpace.ball ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) U : Set β)) →
        Membership.mem (γ := Set ((α →ᵤ[𝔖] β) × α))
          {x_2 : (α →ᵤ[𝔖] β) × α |
            (fun (a : (α →ᵤ[𝔖] β) × α) ↦
                Membership.mem (α := β × β) (SetRel.comp U U)
                  (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f, x).1 (f, x).2))
                      (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) a :
                    β × β))
              x_2}
          x_1}
    a
Tactic: filter_upwards [prod_mem_nhds (UniformOnFun.gen_mem_nhds _ _ _ hV hU)
    (inter_mem hVx <| hc <| UniformSpace.ball_mem_nhds _ hU)]
    with ⟨g, y⟩ ⟨hg, hyV, hy⟩ using ⟨toFun 𝔖 f y, hy, hg y hyV⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
hc : ContinuousAt.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) x
U : Set (β × β)
hU : U ∈ 𝓤 β
V : Set α
hV : V ∈ 𝔖
hVx : V ∈ 𝓝 x
h :
  ∀ (a : (α →ᵤ[𝔖] β) × α),
    Membership.mem (γ := Set ((α →ᵤ[𝔖] β) × α))
      {x_1 : (α →ᵤ[𝔖] β) × α |
        x_1 ∈
            SProd.sprod (α := Set (α →ᵤ[𝔖] β))
              {g : α →ᵤ[𝔖] β |
                ∀ x ∈ V,
                  Membership.mem (α := β × β) U
                    (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
              (V ∩
                preimage.{u_1, u_2} (β := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f : α → β)
                  (UniformSpace.ball ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) U : Set β)) →
          Membership.mem (γ := Set ((α →ᵤ[𝔖] β) × α))
            {x_2 : (α →ᵤ[𝔖] β) × α |
              (fun (a : (α →ᵤ[𝔖] β) × α) ↦
                  Membership.mem (α := β × β) (SetRel.comp U U)
                    (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f, x).1 (f, x).2))
                        (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) a :
                      β × β))
                x_2}
            x_1}
      a
⊢ ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
    Membership.mem (α := β × β) (SetRel.comp U U)
      (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f, x).1 (f, x).2))
          (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) a :
        β × β)
have h₁ : ∀
  a ∈
    SProd.sprod (α := Set (α →ᵤ[𝔖] β))
      {g : α →ᵤ[𝔖] β |
        ∀ x ∈ V,
          Membership.mem (α := β × β) U
            (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
      (V ∩
        preimage.{u_1, u_2} (β := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f : α → β)
          (UniformSpace.ball ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) U : Set β)),
  Membership.mem (α := β × β) (SetRel.comp U U)
    (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x))
        (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) a :
      β × β)
Tactic: filter_upwards [prod_mem_nhds (UniformOnFun.gen_mem_nhds _ _ _ hV hU)
    (inter_mem hVx <| hc <| UniformSpace.ball_mem_nhds _ hU)]
    with ⟨g, y⟩ ⟨hg, hyV, hy⟩ using ⟨toFun 𝔖 f y, hy, hg y hyV⟩
-- 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 : CompleteSpace β
⊢ CompleteSpace (α →ᵤ[𝔖] β)
have inl : IsEmpty β → CompleteSpace (α →ᵤ[𝔖] β)
Tactic: rcases isEmpty_or_nonempty β
-- 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 : CompleteSpace β
inl : IsEmpty β → CompleteSpace (α →ᵤ[𝔖] β)
⊢ CompleteSpace (α →ᵤ[𝔖] β)
have inr : Nonempty β → CompleteSpace (α →ᵤ[𝔖] β)
Tactic: rcases isEmpty_or_nonempty β
-- 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 : CompleteSpace β
h : Nonempty β
⊢ CompleteSpace (α →ᵤ[𝔖] β)
have inr : ∀ {F : Filter (α →ᵤ[𝔖] β)} (hF : Cauchy F), ∃ (x : α →ᵤ[𝔖] β), F ≤ 𝓝 x
Tactic: refine ⟨fun {F} hF ↦ ?_⟩
-- 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 : CompleteSpace β
h : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
⊢ ∃ (x : α →ᵤ[𝔖] β), F ≤ 𝓝 x
have this : F.NeBot
Tactic: have := hF.1
-- 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 : CompleteSpace β
h : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
⊢ ∃ (x : α →ᵤ[𝔖] β), F ≤ 𝓝 x
have this₁ : ∀ 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))
-- 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 : 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)
⊢ ∃ (x : α →ᵤ[𝔖] β), F ≤ 𝓝 x
have inr : ∀ (g : (x : α) → β)
  (hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun (x_1 : α →ᵤ[𝔖] β) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x_1 x) F (𝓝 (g x))),
  ∃ (x : α →ᵤ[𝔖] β), F ≤ 𝓝 x
Tactic: choose! g hg using this
Cleared hypotheses: this
-- 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 : 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))
⊢ ∃ (x : α →ᵤ[𝔖] β), F ≤ 𝓝 x
have h : F ≤ 𝓝 ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) g)
Tactic: use ofFun 𝔖 g
-- 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 : 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))
⊢ F ≤ 𝓝 ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) g)
have 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
Tactic: simp_rw [UniformOnFun.nhds_eq_of_basis _ _ uniformity_hasBasis_closed, le_iInf₂_iff,
      le_principal_iff]
-- 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 β β
⊢ ∀ (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
have 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
Tactic: ⟨hU, hUc⟩