chore(MeasureTheory.Decomposition.Lebesgue): cleaning and a few new b…

…asic lemmas (#11561)

Move lemmas to put similar ones together, replace `refine'` by `refine` and `=>` by `↦`.
Lemmas added:
* `singularPart_add_rnDeriv` and `rnDeriv_add_singularPart`: almost aliases of `haveLebesgueDecomposition_add`
* `haveLebesgueDecomposition_smul'`, `haveLebesgueDecomposition_rnDeriv`
* `singularPart_eq_zero_of_ac`, `singularPart_eq_zero`, `singularPart_self`, `singularPart_eq_self`



Co-authored-by: Rémy Degenne <remydegenne@gmail.com>