feat(MeasureTheory\Group\Action): add μ(c • s ∩ t) = μ(s ∩ c⁻¹ • t) and similar (#32117)

Adding lemmas (and their symmetric version thereof)
`μ(c • s ∩ t) = μ(s ∩ c⁻¹ • t)`
`μ(c • s ∪ t) = μ(s ∪ c⁻¹ • t)`
`μ(c • s ∖ t) = μ(s ∖ c⁻¹ • t)`
`μ(c • s Δ t) = μ(s Δ c⁻¹ • t)`
for μ a `SMulInvariantMeasure`.

Author: ster99

Mathlib/MeasureTheory/Group/Action.lean

@@ -25,7 +25,7 @@ some basic properties of such measures.
 @[expose] public section
 
 
-open scoped ENNReal NNReal Pointwise Topology
+open scoped ENNReal NNReal Pointwise Topology symmDiff
 open MeasureTheory.Measure Set Function Filter
 
 namespace MeasureTheory
@@ -105,6 +105,38 @@ theorem measure_preimage_smul (c : G) (s : Set α) : μ ((c • ·) ⁻¹' s) =
 theorem measure_smul (c : G) (s : Set α) : μ (c • s) = μ s := by
   simpa only [preimage_smul_inv] using measure_preimage_smul μ c⁻¹ s
 
+@[to_additive (attr := simp)]
+theorem measure_inter_inv_smul (c : G) (s t : Set α) : μ (s ∩ c⁻¹ • t) = μ (c • s ∩ t) := by
+  rw [← measure_smul _ c, smul_set_inter, smul_smul, mul_inv_cancel, one_smul]
+
+@[to_additive (attr := simp)]
+theorem measure_inv_smul_inter (c : G) (s t : Set α) : μ (c⁻¹ • s ∩ t) = μ (s ∩ c • t) := by
+  simpa [inv_inv] using (measure_inter_inv_smul _ c⁻¹ _ _).symm
+
+@[to_additive (attr := simp)]
+theorem measure_union_inv_smul (c : G) (s t : Set α) : μ (s ∪ c⁻¹ • t) = μ (c • s ∪ t) := by
+  rw [← measure_smul _ c, smul_set_union, smul_smul, mul_inv_cancel, one_smul]
+
+@[to_additive (attr := simp)]
+theorem measure_inv_smul_union (c : G) (s t : Set α) : μ (c⁻¹ • s ∪ t) = μ (s ∪ c • t) := by
+  simpa [inv_inv] using (measure_union_inv_smul _ c⁻¹ _ _).symm
+
+@[to_additive (attr := simp)]
+theorem measure_sdiff_inv_smul (c : G) (s t : Set α) : μ (s \ c⁻¹ • t) = μ (c • s \ t) := by
+  rw [← measure_smul _ c, smul_set_sdiff, smul_smul, mul_inv_cancel, one_smul]
+
+@[to_additive (attr := simp)]
+theorem measure_inv_smul_sdiff (c : G) (s t : Set α) : μ (c⁻¹ • s \ t) = μ (s \ c • t) := by
+  simpa [inv_inv] using (measure_sdiff_inv_smul _ c⁻¹ _ _).symm
+
+@[to_additive (attr := simp)]
+theorem measure_symmDiff_inv_smul (c : G) (s t : Set α) : μ (s ∆ (c⁻¹ • t)) = μ ((c • s) ∆ t) := by
+  rw [← measure_smul _ c, smul_set_symmDiff, smul_smul, mul_inv_cancel, one_smul]
+
+@[to_additive (attr := simp)]
+theorem measure_inv_smul_symmDiff (c : G) (s t : Set α) : μ ((c⁻¹ • s) ∆ t) = μ (s ∆ (c • t)) := by
+  simpa [inv_inv] using (measure_symmDiff_inv_smul _ c⁻¹ _ _).symm
+
 variable {μ}
 
 @[to_additive]