no goals
α : Type u
β : Type v
inst✝ : UniformSpace α
u : ℕ → α
⊢ CauchySeq u ↔ ∀ (V : Set (α × α)), V ∈ 𝓤 α → ∃ N, ∀ (k : ℕ), k ≥ N → ∀ (l : ℕ), l ≥ N → (u k, u l) ∈ V
simp only [cauchySeq_iff', Filter.eventually_atTop_prod_self', mem_preimage, Prod_map]