feat: break MePo score ties by overlap

[raphael-solace]

This PR makes MePo premise suggestions less likely to rank tiny generic theorems ahead of equally-scored domain-specific lemmas.

MePo now breaks score ties within a single iteration by preferring candidates that share more constants with the current relevant set. This does not change which candidates pass the threshold.

A regression check verifies that Int.add_comm ranks before generic Eq.symm for an integer commutativity goal.

Fixes #13749.

Tests: git diff --check locally. I did not run the Lean test suite locally because this workspace is a shallow sparse checkout without a local Lean toolchain.

[raphael-solace]

I do not have permission to add labels on this repo. This should get \ (or another maintainer-preferred changelog label) to satisfy the PR body check.

[raphael-solace]

Correction: the needed label is changelog-tactics (or another maintainer-preferred changelog label).

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-05-25 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-05-25 12:40:44)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-13834 has successfully built against this PR. (2026-05-25 13:36:29) View Log

[Kha]

Thank you for your contributions but if we want to fix these issues with AI, it will be easier to do it ourselves.