fix: warn when Where is used instead of where in declarations

[kim-em]

This PR fixes a UX bug where writing inductive Foo : Type Where (with capital W) would silently parse Where as a universe level variable, causing confusing downstream errors about "universe level metavariables".

Now the parser accepts both where and Where, but logs a warning when the capitalized form is used. This makes the code work correctly while alerting the user to the typo.

Closes #11853

🤖 Prepared with Claude Code

[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 c358b0c7341de7cdd732b8f09ab552f7405facfb --onto 4e8b5cfc4696efb13c2fb3dc8ae6033197ae2b1f. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-05 11:48:08)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c358b0c7341de7cdd732b8f09ab552f7405facfb --onto 8207919728b9299f43b75e1efd52a6900580819b. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-06 00:03:43)

[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 c358b0c7341de7cdd732b8f09ab552f7405facfb --onto 8207919728b9299f43b75e1efd52a6900580819b. You can force reference manual CI using the force-manual-ci label. (2026-01-05 11:48:10)

[kim-em]

Thanks for the review! I've addressed the suggestions:

1. Renamed to whereKw - can't use «where» as there's already a @[builtin_command_parser] def «where» in this file

2. Removed whereOrWhere' - now using whereKw >> ppSpace for the structure parser

3. Regarding nonReservedSymbol: I tried it, but it doesn't work in this context. nonReservedSymbol is designed for tokens that might also be used as identifiers elsewhere. Here, we actually need Where to be recognized as a keyword to prevent the type parser from consuming it as a universe level (which is the original bug). I've added a comment explaining this.

4. Not touching := - keeping this PR focused on the Where typo issue.