[Merged by Bors] - chore: remove superfluous intros

[mo271]

---

[github-actions]

PR summary 0abc04ad7b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

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

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

[grunweg]

!bench

[grunweg]

FYI, the awaiting-review label was recently removed: you can simply omit it now. (See zulip for details.)

[grunweg]

Thanks for your PR! These changes look good; I have one follow-up request.
Out of paranoia, I'd like to see if this makes any difference performance-wise; otherwise, this is good to go.

[leanprover-bot]

Here are the benchmark results for commit 8ba9e11.
There were no significant changes against commit e242f1e.

[grunweg]

No performance effect - if you fix the nit, this is ready to be merged.

[grunweg]

Thanks again for your contribution!
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