feat(measure_theory/group/basic): make is_[add|mul]_[left|right]_invariant classes (#11655)

* Simplify the definitions of these classes
* Generalize many results about topological groups to measurable groups (still to do in `group/prod`)
* Simplify some proofs
* Make function argument of `integral_mul_[left|right]_eq_self` explicit (otherwise it is hard to apply this lemma in case the function is not a variable)



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: fpvandoorn

src/analysis/fourier.lean

@@ -67,6 +67,7 @@ instance : measurable_space circle := borel circle
 instance : borel_space circle := ⟨rfl⟩
 
 /-- Haar measure on the circle, normalized to have total measure 1. -/
+@[derive is_haar_measure]
 def haar_circle : measure circle := haar_measure positive_compacts_univ
 
 instance : is_probability_measure haar_circle := ⟨haar_measure_self⟩
@@ -205,8 +206,7 @@ begin
   have hij : -i + j ≠ 0,
   { rw add_comm,
     exact sub_ne_zero.mpr (ne.symm h) },
-  exact integral_zero_of_mul_left_eq_neg (is_mul_left_invariant_haar_measure _)
-    (fourier_add_half_inv_index hij)
+  exact integral_zero_of_mul_left_eq_neg (fourier_add_half_inv_index hij)
 end
 
 end monomials