no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : UniformCauchySeqOn F p s
⊢ UniformCauchySeqOnFilter F p (𝓟 s)
rwa [← uniformCauchySeqOn_iff_uniformCauchySeqOnFilter]