case inl
α : Type ?u.555240
β : Type ?u.555243
γ : Type ?u.555246
inst✝ : PseudoEMetricSpace α
a b : ℝ
h : b ≤ a
⊢ EMetric.diam (Ioo a b) = ENNReal.ofReal (b - a)

case inr
α : Type ?u.555240
β : Type ?u.555243
γ : Type ?u.555246
inst✝ : PseudoEMetricSpace α
a b : ℝ
h : a < b
⊢ EMetric.diam (Ioo a b) = ENNReal.ofReal (b - a)
α : Type ?u.555240
β : Type ?u.555243
γ : Type ?u.555246
inst✝ : PseudoEMetricSpace α
a b : ℝ
⊢ EMetric.diam (Ioo a b) = ENNReal.ofReal (b - a)
rcases le_or_lt b a with (h | h)
no goals
case inl
α : Type ?u.555240
β : Type ?u.555243
γ : Type ?u.555246
inst✝ : PseudoEMetricSpace α
a b : ℝ
h : b ≤ a
⊢ EMetric.diam (Ioo a b) = ENNReal.ofReal (b - a)
simp [h]
no goals
case inr
α : Type ?u.555240
β : Type ?u.555243
γ : Type ?u.555246
inst✝ : PseudoEMetricSpace α
a b : ℝ
h : a < b
⊢ EMetric.diam (Ioo a b) = ENNReal.ofReal (b - a)
rw [Real.ediam_eq (bounded_Ioo _ _), csSup_Ioo h, csInf_Ioo h]