feat: add builtin linter sets and make linter.extra a builtin linter set

[wkrozowski]

This PR adds builtin linter sets — linter sets registered from core Lean code during initialization, complementing the user-facing register_linter_set command — and makes linter.extra one of them. Enabling linter.extra (e.g. via set_option linter.extra true or lake lint --extra) now activates the extra linters through the same set-membership mechanism as any other linter set.

The extra linters (dupNamespace, unnecessarySeqFocus, unreachableTactic, unusedDecidableInType) previously relied on dedicated getLinterValueExtra and logLintIfExtra helpers with a special linter.extra fallback; these are removed in favor of the standard getLinterValue/logLintIf. Registering sets from builtin_initialize (before the register_linter_set command elaborator is available) is supported by giving linterSetsExt a LinterSetsState that folds a global builtinLinterSetsRef of builtin sets into every environment, alongside imported and locally-declared entries.

[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-26 15:51:22)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase bf38e594f659ddc5f0bea8b3699d8512dbb99220 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-27 16:57:20)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase cc503a50de7fcc8c3325df6b93647e6a4088f7ee --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-28 13:00:17)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-13852 build failed against this PR. (2026-05-26 15:54:46) View Log
• 🟡 Mathlib branch lean-pr-testing-13852 build against this PR was cancelled. (2026-05-26 16:28:10) View Log
• ✅ Mathlib branch lean-pr-testing-13852 has successfully built against this PR. (2026-05-26 17:20:36) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bf38e594f659ddc5f0bea8b3699d8512dbb99220 --onto 2cd98639c40d2d2a026dd599093b70f55f55ffaf. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-27 16:57:19)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase cc503a50de7fcc8c3325df6b93647e6a4088f7ee --onto 2cd98639c40d2d2a026dd599093b70f55f55ffaf. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-28 13:00:15)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase cc503a50de7fcc8c3325df6b93647e6a4088f7ee --onto c47a0c7cf035381a2bcdd4cdf2442782eb4a5214. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-29 09:48:59)