Pullback of Haar measure along an open embedding

[kbuzzard]

The pullback of Haar measure along a group homomorphism which is also an open embedding is a Haar measure. This is isHaarMeasure_comap_of_isOpenEmbedding in FLT/HaarMeasure/HaarChar/AddEquiv.lean. My instinct is to just fill in the structure fields directly using the fact that they're true on the target.

[DavidLedvinka]

Claim

[DavidLedvinka]

propose #543