no goals
α : Type u
β : Type v
X : Type ?u.546511
ι : Type ?u.546514
inst✝ : PseudoMetricSpace α
x : α
⊢ comap (dist x) atTop ≤ cocompact α
simpa only [dist_comm _ x] using comap_dist_right_atTop_le_cocompact x