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

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

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Author: kim-em

src/Lean/Elab/Inductive.lean

@@ -83,6 +83,9 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (isCoi
     -- https://github.com/leanprover/lean4/issues/5236
     withRef decl[0] <| Linter.logLintIf Linter.linter.deprecated decl[3]
       "`inductive ... :=` has been deprecated in favor of `inductive ... where`"
+  if decl[3][0].isToken "Where" then
+    -- https://github.com/leanprover/lean4/issues/11853
+    withRef decl[3][0] <| logWarning "`Where` should be lowercase `where`"
   return {
     ref             := decl
     shortDeclName   := name

src/Lean/Elab/Structure.lean

@@ -342,6 +342,9 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str
     let cmd := if structStx[0].getKind == ``Parser.Command.classTk then "class" else "structure"
     withRef structStx[0] <| Linter.logLintIf Linter.linter.deprecated structStx[4][0]
       s!"`{cmd} ... :=` has been deprecated in favor of `{cmd} ... where`."
+  if structStx[4][0].isToken "Where" then
+    -- https://github.com/leanprover/lean4/issues/11853
+    withRef structStx[4][0] <| logWarning "`Where` should be lowercase `where`"
   let fieldBinders := if structStx[4].isNone then #[] else structStx[4][2][0].getArgs
   fieldBinders.foldlM (init := #[]) fun (views : Array StructFieldView) fieldBinder => withRef fieldBinder do
     let mut fieldBinder := fieldBinder

src/Lean/Parser/Command.lean

@@ -232,16 +232,20 @@ or an element `head : α` followed by a list `tail : List α`.
 See [Inductive types](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html)
 for more information.
 -/
+-- Parser that accepts both `where` and `Where` (for typo recovery).
+-- We use `symbol` rather than `nonReservedSymbol` because we need `Where` to be
+-- recognized as a keyword to prevent it from being parsed as a universe level.
+def whereKw : Parser := symbol " where" <|> symbol " Where"
 @[builtin_doc] def «inductive» := leading_parser
-  "inductive " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> optional (symbol " :=" <|> " where") >>
+  "inductive " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> optional (symbol " :=" <|> whereKw) >>
   many ctor >> optional (ppDedent ppLine >> computedFields) >> optDeriving
 @[builtin_doc] def «coinductive» := leading_parser
-  "coinductive " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> optional (symbol " :=" <|> " where") >>
+  "coinductive " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> optional (symbol " :=" <|> whereKw) >>
   many ctor >> optional (ppDedent ppLine >> computedFields) >> optDeriving
 def classInductive   := leading_parser
   atomic (group (symbol "class " >> "inductive ")) >>
   recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >>
-  optional (symbol " :=" <|> " where") >> many ctor >> optDeriving
+  optional (symbol " :=" <|> whereKw) >> many ctor >> optDeriving
 def structExplicitBinder := leading_parser
   atomic (declModifiers true >> "(") >>
   withoutPosition (many1 ident >> ppIndent optDeclSig >>
@@ -274,7 +278,7 @@ def «structure»          := leading_parser
     -- Note: no error recovery here due to clashing with the `class abbrev` syntax
     declId >>
     ppIndent (optDeclSig >> optional «extends») >>
-    optional ((symbol " := " <|> " where ") >> optional structCtor >> structFields) >>
+    optional ((symbol " := " <|> whereKw >> ppSpace) >> optional structCtor >> structFields) >>
     optDeriving
 @[builtin_command_parser] def declaration := leading_parser
   declModifiers false >>

tests/lean/run/whereTypoWarning.lean

@@ -0,0 +1,40 @@
+/-!
+# Test for warning when `Where` (capitalized) is used instead of `where`
+
+Relates to: https://github.com/leanprover/lean4/issues/11853
+-/
+
+-- Test that `Where` in inductive is accepted but generates a warning
+/--
+warning: `Where` should be lowercase `where`
+-/
+#guard_msgs in
+inductive MyResult (α : Type) : Type Where
+  | Ok : α → MyResult α
+  | Err : String → MyResult α
+
+-- Verify the inductive works correctly
+#check MyResult.Ok
+#check MyResult.Err
+
+-- Test that `Where` in structure is accepted but generates a warning
+/--
+warning: `Where` should be lowercase `where`
+-/
+#guard_msgs in
+structure MyPoint Where
+  x : Nat
+  y : Nat
+
+-- Verify the structure works correctly
+#check MyPoint.mk
+#check MyPoint.x
+
+-- Test that lowercase `where` does not generate a warning
+inductive MyResult2 (α : Type) : Type where
+  | Ok : α → MyResult2 α
+  | Err : String → MyResult2 α
+
+structure MyPoint2 where
+  x : Nat
+  y : Nat