case inl
α : Type ?u.556633
β : Type ?u.556636
γ : Type ?u.556639
inst✝ : PseudoEMetricSpace α
a b : ℝ
h : a ≤ b
⊢ EMetric.diam (Icc a b) = ENNReal.ofReal (b - a)

case inr
α : Type ?u.556633
β : Type ?u.556636
γ : Type ?u.556639
inst✝ : PseudoEMetricSpace α
a b : ℝ
h : b < a
⊢ EMetric.diam (Icc a b) = ENNReal.ofReal (b - a)
α : Type ?u.556633
β : Type ?u.556636
γ : Type ?u.556639
inst✝ : PseudoEMetricSpace α
a b : ℝ
⊢ EMetric.diam (Icc a b) = ENNReal.ofReal (b - a)
rcases le_or_lt a b with (h | h)
no goals
case inl
α : Type ?u.556633
β : Type ?u.556636
γ : Type ?u.556639
inst✝ : PseudoEMetricSpace α
a b : ℝ
h : a ≤ b
⊢ EMetric.diam (Icc a b) = ENNReal.ofReal (b - a)
rw [Real.ediam_eq (bounded_Icc _ _), csSup_Icc h, csInf_Icc h]
no goals
case inr
α : Type ?u.556633
β : Type ?u.556636
γ : Type ?u.556639
inst✝ : PseudoEMetricSpace α
a b : ℝ
h : b < a
⊢ EMetric.diam (Icc a b) = ENNReal.ofReal (b - a)
simp [h, h.le]