ci: adapt auto-merge check for GitHub apps bots (leanprover-community#34980)

The steps in our build workflow which determine whether to act on the `auto-merge-after-CI` label are [failing](https://github.com/leanprover-community/mathlib4/actions/runs/21793023184/job/62877678664?pr=34967#step:8:11) when one of our new GitHub apps bots has applied the label, since the username no longer corresponds to a user. 

We fix that by whitelisting the bot usernames. ([Usernames must be unique across both bots and users](https://docs.github.com/en/apps/creating-github-apps/registering-a-github-app/registering-a-github-app#registering-a-github-app) so it should be impossible for someone to pose as one of them.)

Noticed in [#nightly-testing > Mathlib &leanprover-community#96;lake update&leanprover-community#96; failure @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20.60lake.20update.60.20failure/near/572616935).

Author: bryangingechen

.github/workflows/build_template.yml

@@ -774,7 +774,10 @@ jobs:
           echo "username=$USERNAME" >> "$GITHUB_OUTPUT"
           echo "Found label actor: $USERNAME"
 
-      - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
+      - if: >- # bot usernames will cause this step to error with "Could not resolve to a User..."
+          contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') &&
+          steps.get-label-actor.outputs.username != 'mathlib-nolints' &&
+          steps.get-label-actor.outputs.username != 'mathlib-update-dependencies'
         name: check team membership
         uses: tspascoal/get-user-teams-membership@57e9f42acd78f4d0f496b3be4368fc5f62696662 # v3.0.0
         id: actorTeams
@@ -784,11 +787,18 @@ jobs:
           username: ${{ steps.get-label-actor.outputs.username }}
           GITHUB_TOKEN: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # (Requires scope: `read:org`)
 
-      # The create-github-app-token README states that this token is masked and will not be logged accidentally.
-      - if: ${{ contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') && (contains(steps.actorTeams.outputs.teams, 'mathlib-maintainers') || contains(steps.actorTeams.outputs.teams, 'bot-users')) }}
+      - if: >-
+          contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') &&
+          (
+            steps.get-label-actor.outputs.username == 'mathlib-nolints' ||
+            steps.get-label-actor.outputs.username == 'mathlib-update-dependencies' ||
+            contains(steps.actorTeams.outputs.teams, 'mathlib-maintainers') ||
+            contains(steps.actorTeams.outputs.teams, 'bot-users')
+          )
         name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
         uses: GrantBirki/comment@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1
         with:
+          # The create-github-app-token README states that this token is masked and will not be logged accidentally.
           token: ${{ steps.auto-merge-app-token.outputs.token }}
           issue-number: ${{ steps.PR.outputs.number }}
           body: |