From 8dfc71c4fdec9db05da080f45596fece57a241cd Mon Sep 17 00:00:00 2001
From: jrr6 <7482866+jrr6@users.noreply.github.com>
Date: Sat, 12 Jul 2025 19:04:02 -0400
Subject: [PATCH] chore: remove superfluous whitespace from error message
 (#9335)

This PR fixes a typo that caused the "cannot infer resulting universe
level of inductive datatype" error message to have leading whitespace.
---
 src/Lean/Elab/MutualInductive.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean
index 25b46e96dd..439c48dee1 100644
--- a/src/Lean/Elab/MutualInductive.lean
+++ b/src/Lean/Elab/MutualInductive.lean
@@ -487,7 +487,7 @@ def shouldInferResultUniverse (u : Level) : TermElabM (Option LMVarId) := do
     match u.getLevelOffset with
     | Level.mvar mvarId => return some mvarId
     | _ =>
-      throwError "
+      throwError "\
         cannot infer resulting universe level of inductive datatype, \
         given resulting type contains metavariables{indentExpr <| mkSort u}\n\
         provide universe explicitly"