mathlib

5aaa5faa - chore(measure_theory/integral/set_integral): update old lemmas that were in comments at the end of the file (#9111)

chore(measure_theory/integral/set_integral): update old lemmas that were in comments at the end of the file (#9111) The file `set_integral` had a list of lemmas in comments at the end of the file, which were written for an old implementation of the set integral. This PR deletes the comments, and adds the corresponding results when they don't already exist. The lemmas `set_integral_congr_set_ae` and `set_integral_mono_set` are also moved to relevant sections. Co-authored-by: RemyDegenne <Remydegenne@gmail.com>