test: identifier completion benchmark

[mhuisi]

Adds a basic identifier completion benchmark so that bugs like the one in #6794 are caught earlier.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3aea0fd810f404f930aa95f9666cf60940bcf64e --onto 69a73a18fbfa1fc045bfbf1c4cf93b155d4c9387. (2025-01-27 18:15:57)

[mhuisi]

!bench

[leanprover-bot]

Here are the benchmark results for commit e86681f.
There were significant changes against commit 3aea0fd:

  Benchmark                   Metric          Change
  ============================================================
+ big_omega.lean              branch-misses    -4.9% (-17.9 σ)
+ big_omega.lean MT           branch-misses    -5.1% (-10.9 σ)
+ bv_decide_inequality.lean   branch-misses    -1.2% (-25.2 σ)
+ bv_decide_mul               branch-misses    -3.1% (-44.7 σ)
+ bv_decide_realworld         branch-misses    -1.4% (-13.4 σ)
+ ilean roundtrip             branch-misses    -3.9% (-11.2 σ)
+ simp_arith1                 branch-misses    -3.2% (-23.0 σ)