∀ {ι : Type u_2} {κ : Type u_3} {G : Type u_6} [inst : SeminormedAddGroup G] {f : ι → κ → G} {l : Filter ι}
  {l' : Filter κ},
  UniformCauchySeqOnFilter f l l' ↔ TendstoUniformlyOnFilter (fun n z => f n.1 z - f n.2 z) 0 (l ×ˢ l) l'