no goals
α : Type u_2
β : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
ι : Type u_3
l : Filter ι
l' : Filter β
f f' : ι → β → α
g g' : β → α
s : Set β
hf : UniformCauchySeqOn f l s
hf' : UniformCauchySeqOn f' l s
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (m : ι × ι) in l ×ˢ l, ∀ (x : β), x ∈ s → ((f / f') m.fst x, (f / f') m.snd x) ∈ u
simpa using (uniformContinuous_div.comp_uniformCauchySeqOn (hf.prod' hf')) u hu