chore(measure_theory/{bochner_integration, simple_func_dense}): Move construction of embedding of L1 simple funcs (#8185)

At the moment, there is a low-level construction in `measure_theory/simple_func_dense` for the approximation of an element of L1 by simple functions, and this is generalized to a more abstract version (with a normed space `L1.simple_func` and a dense linear embedding of this into `L1`) in `measure_theory/bochner_integration`.  #8114 generalized the low-level construction, and I am thinking of rewriting the more abstract version to apply to `Lp`, too.

But since this will all be more generally useful than in the construction of the Bochner integral, and since the Bochner integral file is very long, I propose moving all this material into `measure_theory/simple_func_dense`.  This PR shows what it would look like.  There are no mathematical changes.

Author: hrmacbeth