[Merged by Bors] - chore: add module deprecations for removed files#30519

Ruben-VandeVelde wants to merge 2 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

Ruben-VandeVelde:depr-moveRuben-VandeVelde/mathlib4:depr-moveCopy head branch name to clipboard