fix: remove misleading leading space in " where"

src/Lean/Parser/Command.lean

@@ -90,7 +90,7 @@ def declValEqns      := leading_parser
 def whereStructField := leading_parser
   Term.letDecl
 def whereStructInst  := leading_parser
-  " where" >> sepByIndent (ppGroup whereStructField) "; " (allowTrailingSep := true) >>
+  ppIndent ppSpace >> "where" >> sepByIndent (ppGroup whereStructField) "; " (allowTrailingSep := true) >>
   optional Term.whereDecls
 /-
   Remark: we should not use `Term.whereDecls` at `declVal`

src/Lean/Parser/Term.lean

@@ -495,7 +495,7 @@ def «letrec» := leading_parser:leadPrec
 
 @[run_builtin_parser_attribute_hooks]
 def whereDecls := leading_parser
-  " where" >> sepBy1Indent (ppGroup letRecDecl) "; " (allowTrailingSep := true)
+  "where" >> sepBy1Indent (ppGroup letRecDecl) "; " (allowTrailingSep := true)
 
 @[run_builtin_parser_attribute_hooks]
 def matchAltsWhereDecls := leading_parser

tests/lean/formatTerm.lean

@@ -52,3 +52,10 @@ set_option format.indent 4 in
 #eval fmt `(let x := { foo := bar
                        bar := foo + bar }
             x)
+
+#eval fmt `(command|
+def foo : a b c d e f g a b c d e f g h where
+  h := 42
+  i := 42
+  j := 42
+  k := 42)

tests/lean/formatTerm.lean.expected.out

@@ -61,3 +61,9 @@ let x✝ :=
   { foo✝ := bar✝
     bar✝ := foo✝ + bar✝ }
 x✝
+def foo✝ : a✝ b✝ c✝ d✝ e✝ f✝ g✝ a✝ b✝ c✝ d✝ e✝ f✝ g✝ h✝
+    where
+  h✝ := 42
+  i✝ := 42
+  j✝ := 42
+  k✝ := 42