refactor(*): supremum of several recent refactoring PRs (#17381)
This is the supremum of
* #17376
* #17375
* #17374
* #17362
* #17355
* #17349
* #17347
* #17338
* #17336
with imports fixed up to accommodate all the overlapping changes to imports.
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>
mathlib3
f7707875 - refactor(*): supremum of several recent refactoring PRs (#17381)
