no goals
α✝ : Type ?u.431607
β : Type ?u.431610
γ : Type ?u.431613
inst✝¹ : PseudoEMetricSpace α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
⊢ diam (closure s) = diam s
simp only [Metric.diam, EMetric.diam_closure]