fix: use mathlib-lean-pr-testing app for PR comments

This PR fixes the PR release workflow which was failing due to the
deprecated `MATHLIB4_COMMENT_BOT` PAT being invalid.

Changes:
- Generate a token from the `mathlib-lean-pr-testing` GitHub App for
  posting comments to Lean PRs about mathlib compatibility
- Use `GITHUB_TOKEN` for read-only label fetching
- Update the bot username check from `leanprover-community-bot` to
  `mathlib-lean-pr-testing[bot]`

Requires `MATHLIB_LEAN_PR_TESTING_APP_ID` and
`MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY` secrets (now added).

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
1 file changed