mathlib3

b1859b6d - feat(measure_theory/measure/hausdorff): `(μH[1] : measure ℝ) = volume` (#18982)

feat(measure_theory/measure/hausdorff): `(μH[1] : measure ℝ) = volume` (#18982) And similarly for `(μH[2] : measure ℝ × ℝ) = volume`. This addresses the TODO comment in the docstring. The `hausdorff_measure_pi_real` proof has been moved to the bottom of the file so that it can be kept next to the new results.