[Merged by Bors] - feat(measure_theory/integral/set_to_l1): various properties of the set_to_fun construction

[RemyDegenne]

---

[sgouezel]

This looks very good to me. I am only wondering whether this can be used to remove the proofs of some statements about the Bochner integral, replacing them with a call to the more general statement. But this should definitely be done in another PR, this one is already big enough.
bors d+

[bors]

✌️ RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[RemyDegenne]

Thanks for the review!

This looks very good to me. I am only wondering whether this can be used to remove the proofs of some statements about the Bochner integral, replacing them with a call to the more general statement. But this should definitely be done in another PR, this one is already big enough.

See PR #10717 :)

[RemyDegenne]

The "Run tests" CI keeps failing and I don't understand what happens. At the export as low-level text file step, I get the error

Run lean --recursive --export=mathlib.txt src/
<unknown>:1:1: error: unknown declaration '_private.3627408217.add'
Error: Process completed with exit code 1.

[RemyDegenne]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests