no goals
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
⊢ ↑(Measure.toBoxAdditive volume) I = ∏ i : ι, (upper I i - lower I i)
rw [Measure.toBoxAdditive_apply, coe_eq_pi, Real.volume_pi_Ioc_toReal I.lower_le_upper]