no goals
α : Type u
β : Type v
X : Type ?u.432936
ι : Type ?u.432939
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
⊢ Tendsto (dist x) (cocompact α) atTop
simpa only [dist_comm] using tendsto_dist_right_cocompact_atTop x