feat(measure_theory/measure): add a measure_space instance for subtype (#16708)
feat(measure_theory/measure): add a measure_space instance for subtype (#16708)

Using the comap definition added in #15343.
This was predominantly written by Rémy Degenne, and has applications in #2819.

Co-authored-by: Rémy Degenne <remydegenne@gmail.com>



Co-authored-by: RemyDegenne <d1cbd7c6b2e8ace9cf5ebccbf5e625f4abf38ca0@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib