[Merged by Bors] - chore: delete obsolete porting scripts

[kim-em]

This is a more conservative version of #14314, deleting just the scripts that we should have deleted a year ago when the port finished.

[github-actions]

PR summary b77b26f730

Import changes

No significant changes to the import graph

---

Declarations diff

- condense(s):
- get_mathlib4_module_commit_info(contents):
- mk_label(path:
- update_file_header(file_path):

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[kim-em]

See @grunweg's analysis at #14314 (review) confirming these scripts are all only useful during the port. He didn't include benchmark.sh, which I've also deleted here. This was solely to provide comparative benchmarking of the ported subset of mathlib3. (I wrote it.)

[grunweg]

Thanks for elaborating on benchmarks.sh, that context is definitely useful to have :-)
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style