chore(measure_theory/integral/lebesgue): use to_additive when declaring instances and basic lemmas about simple functions (#12000)
chore(measure_theory/integral/lebesgue): use to_additive when declaring instances and basic lemmas about simple functions (#12000)

I also grouped similar lemmas together and added one or two missing ones.





leanprover-community/mathlib,leanprover-community/mathlib