Restriction of translation-invariant measures to a subgroup

[YaelDillies]

Let $G$ be a measurable group, $H$ a subgroup of $G$ and $\mu$ a left (resp. right) translation-invariant measure. Then $H$ is a measurable group and $\mu$ restricted to $H$ is a left (resp. right) translation-invariant measure.

These will be sorrys in FLT/Mathlib/MeasureTheory/Group/Action.lean once #223 is merged.