mathlib

e25981a8 - feat(measure_theory/measure/measure_space): `volume_preimage_coe` (#17030)

feat(measure_theory/measure/measure_space): `volume_preimage_coe` (#17030) This is another lemma needed by #2819, I'm not sure exactly of its provenance, but it looks like @YaelDillies extracted it as a lemma at least, if not wrote the original version completely. Co-authored-by: Yaël Dillies [yael.dillies@gmail.com](mailto:yael.dillies@gmail.com) Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>