case pos
ι : Type ?u.374130
inst✝ : Fintype ι
s : Set ℝ
hs : Metric.Bounded s
⊢ ↑↑volume s ≤ EMetric.diam s

case neg
ι : Type ?u.374130
inst✝ : Fintype ι
s : Set ℝ
hs : ¬Metric.Bounded s
⊢ ↑↑volume s ≤ EMetric.diam s
ι : Type ?u.374130
inst✝ : Fintype ι
s : Set ℝ
⊢ ↑↑volume s ≤ EMetric.diam s
by_cases hs : Metric.Bounded s
case pos
ι : Type ?u.374130
inst✝ : Fintype ι
s : Set ℝ
hs : Metric.Bounded s
⊢ ↑↑volume s ≤ ↑↑volume (Icc (sInf s) (sSup s))
case pos
ι : Type ?u.374130
inst✝ : Fintype ι
s : Set ℝ
hs : Metric.Bounded s
⊢ ↑↑volume s ≤ EMetric.diam s
rw [Real.ediam_eq hs, ← volume_Icc]
no goals
case pos
ι : Type ?u.374130
inst✝ : Fintype ι
s : Set ℝ
hs : Metric.Bounded s
⊢ ↑↑volume s ≤ ↑↑volume (Icc (sInf s) (sSup s))
exact volume.mono (Real.subset_Icc_sInf_sSup_of_bounded hs)
case neg
ι : Type ?u.374130
inst✝ : Fintype ι
s : Set ℝ
hs : ¬Metric.Bounded s
⊢ ↑↑volume s ≤ ⊤
case neg
ι : Type ?u.374130
inst✝ : Fintype ι
s : Set ℝ
hs : ¬Metric.Bounded s
⊢ ↑↑volume s ≤ EMetric.diam s
rw [Metric.ediam_of_unbounded hs]
no goals
case neg
ι : Type ?u.374130
inst✝ : Fintype ι
s : Set ℝ
hs : ¬Metric.Bounded s
⊢ ↑↑volume s ≤ ⊤
exact le_top