feat(measure_theory/haar_measure): Prove uniqueness (#5663)
Prove the uniqueness of Haar measure (up to a scalar) following *Measure Theory* by Paul Halmos. This proof seems to contain an omission which we fix by adding an extra hypothesis to an intermediate lemma.
Add some lemmas about left invariant regular measures.
We add the file `measure_theory.prod_group` which contain various measure-theoretic properties of products of topological groups, needed for the uniqueness.
We add `@[to_additive]` to some declarations in `measure_theory`, but leave it out for many because of #4210. This causes some renamings in concepts, like `is_left_invariant` -> `is_mul_left_invariant` and `measure.conj` -> `measure.inv` (though a better naming suggestion for this one is welcome).
