feat: add MeasureTheory.inv_smul_ae_eq_self (#5429)

- Add `MeasureTheory.inv_smul_ae_eq_self` and its additive version.
- Add `@[to_additive]` to `MeasureTheory.measure_smul_null`.

- Fix the order of implicit arguments and universes in
  `MeasureTheory.vadd_ae_eq_self_of_mem_zmultiples` to match the
  multiplicative version.

Mathlib/MeasureTheory/Group/Action.lean

@@ -27,7 +27,9 @@ open ENNReal NNReal Pointwise Topology MeasureTheory MeasureTheory.Measure Set F
 
 namespace MeasureTheory
 
-variable {G M α : Type _} {s : Set α}
+universe u v w
+
+variable {G : Type u} {M : Type v} {α : Type w} {s : Set α}
 
 /-- A measure `μ : Measure α` is invariant under an additive action of `M` on `α` if for any
 measurable set `s : Set α` and `c : M`, the measure of its preimage under `fun x => c +ᵥ x` is equal
@@ -197,6 +199,7 @@ theorem NullMeasurableSet.smul {s} (hs : NullMeasurableSet s μ) (c : G) :
 #align measure_theory.null_measurable_set.smul MeasureTheory.NullMeasurableSet.smul
 #align measure_theory.null_measurable_set.vadd MeasureTheory.NullMeasurableSet.vadd
 
+@[to_additive]
 theorem measure_smul_null {s} (h : μ s = 0) (c : G) : μ (c • s) = 0 := by rwa [measure_smul]
 #align measure_theory.measure_smul_null MeasureTheory.measure_smul_null
 
@@ -274,8 +277,9 @@ theorem smul_ae_eq_self_of_mem_zpowers {x y : G} (hs : (x • s : Set α) =ᵐ[
   simpa only [MulAction.toPermHom_apply, MulAction.toPerm_apply, image_smul] using h
 #align measure_theory.smul_ae_eq_self_of_mem_zpowers MeasureTheory.smul_ae_eq_self_of_mem_zpowers
 
-theorem vadd_ae_eq_self_of_mem_zmultiples {G : Type _} [MeasurableSpace G] [AddGroup G]
-    [AddAction G α] [VAddInvariantMeasure G α μ] [MeasurableVAdd G α] {x y : G}
+theorem vadd_ae_eq_self_of_mem_zmultiples {G : Type u} {α : Type w} {s : Set α}
+    {m : MeasurableSpace α} [AddGroup G] [AddAction G α] [MeasurableSpace G] [MeasurableVAdd G α]
+    {μ : Measure α} [VAddInvariantMeasure G α μ] {x y : G}
     (hs : (x +ᵥ s : Set α) =ᵐ[μ] s) (hy : y ∈ AddSubgroup.zmultiples x) :
     (y +ᵥ s : Set α) =ᵐ[μ] s := by
   letI : MeasurableSpace (Multiplicative G) := (inferInstanceAs (MeasurableSpace G))
@@ -291,4 +295,8 @@ theorem vadd_ae_eq_self_of_mem_zmultiples {G : Type _} [MeasurableSpace G] [AddG
 
 attribute [to_additive existing vadd_ae_eq_self_of_mem_zmultiples] smul_ae_eq_self_of_mem_zpowers
 
+@[to_additive]
+theorem inv_smul_ae_eq_self {x : G} (hs : (x • s : Set α) =ᵐ[μ] s) : (x⁻¹ • s : Set α) =ᵐ[μ] s :=
+  smul_ae_eq_self_of_mem_zpowers hs <| inv_mem (Subgroup.mem_zpowers _)
+
 end MeasureTheory