no goals
ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
h : a ≤ b
⊢ ENNReal.toReal (↑↑volume (Icc a b)) = ∏ i : ι, (b i - a i)
simp only [volume_Icc_pi, ENNReal.toReal_prod, ENNReal.toReal_ofReal (sub_nonneg.2 (h _))]