[Merged by Bors] - feat: subscript and superscript delaborators

[gio256]

We add the functions delabSubscript and delabSuperscript in the Mathlib.Tactic namespace. These delaborators are triggered only if the entirety of the provided expression can be subscripted (respectively, superscripted).

The delaborators are not exhaustive, in that they will not successfully delaborate every expression that is valid in a subscript or superscript. We instead aim to make them overly conservative, so that any expression which is successfully delaborated must be subscriptable (or superscriptable).

---

This PR is intended to serve as a predecessor to #20719.

[github-actions]

PR summary fb95ea212c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Nat'
+ Nat'.γ
+ delabSubscript
+ delabSuperscript

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[joneugster]

The delaborator look good to me, thanks!

I suggest

maintainer merge

[github-actions]

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

[kmill]

Thanks! Sorry this took so long to get through review.

For sake of not adding any more delay, I took the liberty of pushing some changes to preserve the intent of using decl_name%. The point of it is to ensure that the parser kinds are unique (small detail: it's ``superscript, not `superscript, which causes it to refer to Mathlib.Tactic.superscript). The PR is now more clearly adding delaborators without needing to touch parsers.

If the changes are to your satisfaction, please go ahead and merge! I'm delegating to you @gio256.

bors d+

[mathlib-bors]

✌️ gio256 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[gio256]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style