Theorem: Real.volume_uIoc (Carleson/Theorem1_1/Hilbert_kernel.lean)

State before:
a b : ℝ
⊢ MeasureTheory.volume (Ι a b) = ENNReal.ofReal |b - a|
Tactic:
rw [Set.uIoc, volume_Ioc, max_sub_min_eq_abs]
State after:
no goals