no goals
𝓕 : Type ?u.514878
𝕜 : Type ?u.514881
α : Type ?u.514884
ι : Type u_2
κ : Type u_1
E : Type ?u.514893
F : Type ?u.514896
G : Type u_3
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s✝ : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : ι → κ → G
s : Set κ
l : Filter ι
⊢ UniformCauchySeqOn f l s ↔ TendstoUniformlyOn (fun n z => f n.fst z / f n.snd z) 1 (l ×ˢ l) s
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter,
  uniformCauchySeqOn_iff_uniformCauchySeqOnFilter,
  SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one]