Pulling a.e. statements from AddCircle back to ℝ in Mathlib

To turn '∀ᵐ y : UnitAddCircle, P y' into '∀ᵐ x : ℝ, P ↑x' (e.g. Borel normal numbers from Birkhoff applied to z ↦ q • z, which is ergodic_nsmul), show that the quotient map pulls null sets back to null sets. Replace S by toMeasurable volume S, cover ℝ by the intervals Ioc m (m+1) for m : ℤ (point x lies in the one with m = ⌈x⌉ - 1), and on each one use AddCircle.measurePreserving_mk (m : ℝ). That lemma is MeasurePreserving from volume.restrict (Ioc m (m+1)), so rewrite with ← Measure.restrict_apply (the order is preimage ∩ Ioc, so do not apply inter_comm first) and then hmp.measure_preimage. Finish with measure_iUnion_null and ae_iff.