no goals
α : Type ?u.564058
β : Type ?u.564061
γ : Type ?u.564064
inst✝ : PseudoEMetricSpace α
a b : ℝ
h : a ≤ b
⊢ Metric.diam (Ioc a b) = b - a
simp [Metric.diam, ENNReal.toReal_ofReal (sub_nonneg.2 h)]