mathlib

ad7038e5 - refactor(*): supremum of refactoring PRs #17384 #17398 #17406 #17407 #17408 (#17405)

refactor(*): supremum of refactoring PRs #17384 #17398 #17406 #17407 #17408 (#17405) This is going to be another combination PR. If at any point every constituent PR has been delegated, and I have a green check here, I will hand it to bors (i.e. without waiting for an explicit approval of this PR). The only difference relative to the constituent PRs are any further import adjustments required to keep everything working together. Using this PR means I can locally build everything together to check for interactions. Depends on * [X] #17384 * [X] #17398 * [ ] #17406 * [ ] #17407 * [ ] #17408 Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>