refactor: golf 100 files

[yuanyi-350]

This PR is an experimental project. In this PR, we use an Agent to automatically scan and attempt to simplify proofs. We hope to eventually effectively golf 100 files and avoid reinventing the wheel in mathlib.

We have chosen Mathlib/Analysis as the testing ground. There are currently 785 files in total, and we have scanned 122 so far.

If this experiment is very successful and accepted by the mathlib community, we would be honored to open source it.

• depends on: chore(Analysis/Convex/Approximation): reuse sSup_of_nat_affine_eq #37981
• depends on: chore(Analysis): golf files in Mathlib/Analysis/CStarAlgebra #37987

---

[github-actions]

PR summary 1a3500f1bf

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/pr_summary/declarations_diff.sh <optional_commit>

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

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

---

Decrease in tech debt: (relative, absolute) = (3.00, 0.00)

Current number	Change	Type
6453	-3	backward.isDefEq.respectTransparency

Current commit ffe171fe74
Reference commit 1a3500f1bf

You can run this locally as

./scripts/reporting/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).

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[themathqueen]

I know this is marked WIP, but I just want to say that you should split this into multiple PRs when you're ready. Other golfing PRs usually golf about 5-10 results per PR (I think), so maybe aim for that?

[yuanyi-350]

I know this is marked WIP, but I just want to say that you should split this into multiple PRs when you're ready. Other golfing PRs usually golf about 5-10 results per PR (I think), so maybe aim for that?

@themathqueen , Thank you for your suggestion. We will split this into many PRs for easier maintenance. The purpose of this PR is to serve as a catalog and to demonstrate the golfing potential of mathlib4.

[mathlib-dependent-issues]

This PR/issue depends on:

• chore(Analysis/Convex/Approximation): reuse sSup_of_nat_affine_eq #37981
• chore(Analysis): golf files in Mathlib/Analysis/CStarAlgebra #37987
  By Dependent Issues (🤖). Happy coding!