refactor: golf proofs (stacked on #1332)

[Vilin97]

Golfs proofs across Physlib: streamlining arguments, using stronger mathlib lemmas and tactics, removing redundant steps, and increasing code reuse. No statements or definitions are changed — only proofs.

Rebased directly onto master (previously stacked on the now-closed #1332; all of that PR's golfs have been dropped — this PR's diff is exclusively its own work).

Stats

• Proofs golfed: ~1,343 across 120 files
• Net line change (proof bodies only): −5,954 (9,369 deletions, 3,415 insertions)
• Verification: every touched file recompiled with -Dwarn.sorry=false -Dweak.says.verify=true; full lake build green on the rebased tree; every diff hunk lies strictly inside a proof body (statements/definitions byte-identical).

Process disclosure (per AI-POLICY.md)

• Models: golfing subagents ran on Claude Fable 5 (claude-fable-5) and Claude Opus 4.8 (claude-opus-4-8). One max-reasoning subagent per file, each self-verifying via a per-file lake env lean compile with the CI flags.
• Wall-clock time: ~39h wall-clock (spanning session-limit resets)
• Token usage (approximate, output tokens across all agents): ~19M subagent output tokens

Prompt used

Golf AS MUCH AS POSSIBLE in Physlib. Update PR #1364.
Do not change statements, and do not cram tactics on one line. Genuinely make proofs
shorter and simpler by streamlining arguments, increasing mathlib usage, reduce code duplication, increase code reuse, use more powerful tactics, etc. Do not change any statements and definitions - only work on proofs!
Keep RAM usage under 40GB. Be thorough, go project by project carefully. If spawning agents, use max reasoning, and tell them to be very
thorough. DO NOT ASK ME ANYTHING AND DO NOT GIVE UP, KEEP FINDING NEW WAYS TO COMPRESS.
Open a draft PR once you golfed 50 proofs, and then every 10, update the PR. Put
this prompt in the PR description and also model name and how long and how many tokens this golfing process took.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.