no goals
α : Type u
β : Type v
X : Type ?u.534313
ι : Type ?u.534316
inst✝¹ : PseudoMetricSpace α
s : Set α
x y z : α
inst✝ : ProperSpace α
⊢ EMetric.diam univ = ⊤ ↔ NoncompactSpace α
rw [← not_compactSpace_iff, compactSpace_iff_bounded_univ, bounded_iff_ediam_ne_top,
  Classical.not_not]