no goals
α : Type u
β : Type v
inst✝ : UniformSpace α
l : Filter β
f : β → α
⊢ Cauchy (map f l) ↔ NeBot l ∧ Tendsto (fun p => (f p.fst, f p.snd)) (l ×ˢ l) (𝓤 α)
rw [Cauchy, map_neBot_iff, prod_map_map_eq, Tendsto]