no goals
α : Type u
β : Type v
X : Type ?u.508607
ι : Type ?u.508610
inst✝ : PseudoMetricSpace α
x : α
s t : Set α
r : ℝ
f : ℕ → α
hf : CauchySeq f
⊢ Cauchy (map f Filter.cofinite)
rwa [Nat.cofinite_eq_atTop]