chore: check for empty PRs in CI

[kim-em]

This PR adds a CI check that fails when a PR introduces no changes compared to its base branch. This catches cases where a duplicate PR is queued for merge after an identical PR has already landed (as happened with #12876 and #12877).

The check is added as a second job in the existing check-stage0.yml workflow, which already has the same trigger conditions and git setup pattern. On pull_request events it diffs against the merge base; on merge_group events it diffs HEAD^1..HEAD (the PR's contribution to the synthetic merge commit). Note that batched merge groups are treated as a unit — if the entire group is non-empty the check passes, which is the right behaviour for lean4's typical single-PR queuing.

🤖 Prepared with Claude Code

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bf4f51e70471a4828855f69967345c27869ad2ad --onto 6714601ee4a123fef0f6ff3e44f01086ba78dfce. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-18 00:58:24)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase bf4f51e70471a4828855f69967345c27869ad2ad --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-18 00:58:26)

[Kha]

The check is added as a second job in the existing check-stage0.yml workflow

This doesn't appear to be the case? I think grouping could be good for performance but we should rename the file then