feat: add support for Nat.log2 in simp and cbv

[Rob23oba]

This PR adds support for Nat.log2 in simp (through a new simproc Nat.reduceLog2) and cbv. However, instead of just relying on the kernel to reduce the definition Nat.log2, we use a specialized lemma to reduce the problem Nat.log2 a = b to a (simpler for the kernel) problem 2^b <= a < 2^(b+1). This already produces speedups for small numbers that get more significant the larger the number is. For example:

example : Nat.log2 (1 <<< 100000 + 3) = 100000 := by decide +kernel

(i.e. evaluation by reduction) takes roughly 3 seconds while

example : Nat.log2 (1 <<< 100000 + 3) = 100000 := by cbv

now solves the same goal in a few milliseconds. This will especially prove useful for evaluating floating point operations using cbv since these use Nat.log2 frequently.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-06-10 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-06-14 20:28:43)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-14047 has successfully built against this PR. (2026-06-14 21:24:30) View Log