chore(MeasureTheory): Move lemmas and deprecate duplicates

[D-Thomine]

This PR moves a few lemmas around in MeasureTheory.Measure; basically, if a lemma can be expressed and proved elementarily, it is moved upstream. For instance, if a lemma has μ ≤ ν has an hypothesis, it may be proved as a special case of a lemma about absolutely continuous measures, but may also be proved as easily by more elementary considerations, which means it can be moved to more suitable files upstream (e.g. to MeasureTheory.Measure.MeasureSpace instead of MeasureTheory.Measure.AbsolutelyContinuous).

This also slightly simplifies imports and allowed me to detect two exact duplicates.

---

[github-actions]

PR summary 18a192673a

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.Measure.Comap	1524	1521	-3 (-0.20%)

Import changes for all files

Files	Import difference
Mathlib.MeasureTheory.Measure.Comap	-3

---

Declarations diff (regex)

+ _root_.AEMeasurable.mono_measure
+ _root_.MeasureTheory.ae_restrict_le
+ ae_eq_comp
- Measure.QuasiMeasurePreserving.ae_eq_comp
- ae_restrict_le
- mono_measure

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 18a1926).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 18a192673a
Reference commit 32beea3cad

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).