diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 213e691e9e..bc7c5ad77e 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -46,14 +46,15 @@ register_builtin_option Elab.async : Bool := {
 
 /--
 If the `diagnostics` option is not already set, gives a message explaining this option.
-Begins with a `\n`, so an error message can look like `m!"some error occurred{useDiagnosticMsg}"`.
+Begins with a `\n\n`, so an error message can look like `m!"some error occurred{useDiagnosticMsg}"`.
+The double newline gives better visual separation from the main error message
 -/
 def useDiagnosticMsg : MessageData :=
   MessageData.lazy fun ctx =>
     if diagnostics.get ctx.opts then
       pure ""
     else
-      pure s!"\nAdditional diagnostic information may be available using the `set_option {diagnostics.name} true` command."
+      pure s!"\n\nAdditional diagnostic information may be available using the `set_option {diagnostics.name} true` command."
 
 namespace Core
 
diff --git a/tests/lean/1007.lean.expected.out b/tests/lean/1007.lean.expected.out
index fa277fe368..19a74abe8f 100644
--- a/tests/lean/1007.lean.expected.out
+++ b/tests/lean/1007.lean.expected.out
@@ -8,4 +8,5 @@
 1007.lean:39:4-39:7: warning: declaration uses 'sorry'
 1007.lean:56:64-56:78: error: failed to synthesize
   IsLin fun x => sum fun i => norm x
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
diff --git a/tests/lean/1102.lean.expected.out b/tests/lean/1102.lean.expected.out
index e9902f291b..16d28d938a 100644
--- a/tests/lean/1102.lean.expected.out
+++ b/tests/lean/1102.lean.expected.out
@@ -1,3 +1,4 @@
 1102.lean:22:35-22:49: error: failed to synthesize
   DVR 1
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
diff --git a/tests/lean/2273.lean.expected.out b/tests/lean/2273.lean.expected.out
index 9468bf4cc9..0a85fadb82 100644
--- a/tests/lean/2273.lean.expected.out
+++ b/tests/lean/2273.lean.expected.out
@@ -1,3 +1,4 @@
 2273.lean:9:8-9:14: error: failed to synthesize
   P 37
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
diff --git a/tests/lean/297.lean.expected.out b/tests/lean/297.lean.expected.out
index 6642b1ddb1..20403050ae 100644
--- a/tests/lean/297.lean.expected.out
+++ b/tests/lean/297.lean.expected.out
@@ -3,4 +3,5 @@
 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
   Sort ?u
 due to the absence of the instance above
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
diff --git a/tests/lean/386.lean.expected.out b/tests/lean/386.lean.expected.out
index 321c7108d3..e1f07d7e37 100644
--- a/tests/lean/386.lean.expected.out
+++ b/tests/lean/386.lean.expected.out
@@ -1,3 +1,4 @@
 386.lean:9:2-9:46: error: failed to synthesize
   Fintype ?m
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
diff --git a/tests/lean/448.lean.expected.out b/tests/lean/448.lean.expected.out
index e9f6d96501..0349867478 100644
--- a/tests/lean/448.lean.expected.out
+++ b/tests/lean/448.lean.expected.out
@@ -1,3 +1,4 @@
 448.lean:21:2-23:20: error: failed to synthesize
   MonadExceptOf IO.Error M
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
diff --git a/tests/lean/attrCmd.lean.expected.out b/tests/lean/attrCmd.lean.expected.out
index 37bca849b6..eb7291c07c 100644
--- a/tests/lean/attrCmd.lean.expected.out
+++ b/tests/lean/attrCmd.lean.expected.out
@@ -1,3 +1,4 @@
 attrCmd.lean:6:0-6:6: error: failed to synthesize
   Pure M
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
diff --git a/tests/lean/calcErrors.lean.expected.out b/tests/lean/calcErrors.lean.expected.out
index cdd831923c..b5ce9626ca 100644
--- a/tests/lean/calcErrors.lean.expected.out
+++ b/tests/lean/calcErrors.lean.expected.out
@@ -12,6 +12,7 @@ calcErrors.lean:24:8-24:11: error: invalid 'calc' step, relation expected
   p a
 calcErrors.lean:31:8-31:13: error: invalid 'calc' step, failed to synthesize `Trans` instance
   Trans p p ?m
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 calcErrors.lean:41:7-41:12: error: invalid 'calc' step, left-hand side is
   γ : Sort u_1
diff --git a/tests/lean/defInst.lean.expected.out b/tests/lean/defInst.lean.expected.out
index 7655b755a4..10d38acfae 100644
--- a/tests/lean/defInst.lean.expected.out
+++ b/tests/lean/defInst.lean.expected.out
@@ -1,6 +1,7 @@
 [4, 5, 6]
 defInst.lean:8:26-8:32: error: failed to synthesize
   BEq Foo
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 fun x y => sorry : (x y : Foo) → ?m x y
 [4, 5, 6]
diff --git a/tests/lean/defaultInstance.lean.expected.out b/tests/lean/defaultInstance.lean.expected.out
index 11d9930097..f7ba55e142 100644
--- a/tests/lean/defaultInstance.lean.expected.out
+++ b/tests/lean/defaultInstance.lean.expected.out
@@ -1,5 +1,6 @@
 defaultInstance.lean:20:20-20:23: error: failed to synthesize
   Foo Bool (?m x)
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 defaultInstance.lean:22:35-22:38: error: typeclass instance problem is stuck, it is often due to metavariables
   Foo Bool (?m x)
diff --git a/tests/lean/eagerUnfoldingIssue.lean.expected.out b/tests/lean/eagerUnfoldingIssue.lean.expected.out
index cab207bb69..7de3e27d77 100644
--- a/tests/lean/eagerUnfoldingIssue.lean.expected.out
+++ b/tests/lean/eagerUnfoldingIssue.lean.expected.out
@@ -1,6 +1,8 @@
 eagerUnfoldingIssue.lean:6:2-6:17: error: failed to synthesize
   MonadLog (StateM Nat)
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 eagerUnfoldingIssue.lean:12:2-12:17: error: failed to synthesize
   MonadLog (StateM Nat)
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
diff --git a/tests/lean/eraseInsts.lean.expected.out b/tests/lean/eraseInsts.lean.expected.out
index 7f87845271..d789a552a4 100644
--- a/tests/lean/eraseInsts.lean.expected.out
+++ b/tests/lean/eraseInsts.lean.expected.out
@@ -1,3 +1,4 @@
 eraseInsts.lean:12:22-12:27: error: failed to synthesize
   HAdd Foo Foo ?m
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
diff --git a/tests/lean/forErrors.lean.expected.out b/tests/lean/forErrors.lean.expected.out
index f08536e449..79a034fb50 100644
--- a/tests/lean/forErrors.lean.expected.out
+++ b/tests/lean/forErrors.lean.expected.out
@@ -1,3 +1,4 @@
 forErrors.lean:3:29-3:30: error: failed to synthesize
   ToStream α ?m
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
diff --git a/tests/lean/interactive/4880.lean.expected.out b/tests/lean/interactive/4880.lean.expected.out
index de96f1cf48..c98090e749 100644
--- a/tests/lean/interactive/4880.lean.expected.out
+++ b/tests/lean/interactive/4880.lean.expected.out
@@ -17,7 +17,7 @@
    {"start": {"line": 16, "character": 12},
     "end": {"line": 17, "character": 0}},
    "message":
-   "failed to synthesize\n  A\nAdditional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "failed to synthesize\n  A\n\nAdditional diagnostic information may be available using the `set_option diagnostics true` command.",
    "fullRange":
    {"start": {"line": 16, "character": 12},
     "end": {"line": 20, "character": 0}}},
@@ -37,7 +37,7 @@
    {"start": {"line": 22, "character": 17},
     "end": {"line": 22, "character": 20}},
    "message":
-   "failed to synthesize\n  A\nAdditional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "failed to synthesize\n  A\n\nAdditional diagnostic information may be available using the `set_option diagnostics true` command.",
    "fullRange":
    {"start": {"line": 22, "character": 17},
     "end": {"line": 22, "character": 20}}},
diff --git a/tests/lean/kernelMVarBug.lean.expected.out b/tests/lean/kernelMVarBug.lean.expected.out
index 8a6972e4d3..038285b812 100644
--- a/tests/lean/kernelMVarBug.lean.expected.out
+++ b/tests/lean/kernelMVarBug.lean.expected.out
@@ -1,3 +1,4 @@
 kernelMVarBug.lean:5:15-5:20: error: failed to synthesize
   HAdd α α α
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
diff --git a/tests/lean/macroStack.lean.expected.out b/tests/lean/macroStack.lean.expected.out
index 686732ebd8..53015575c4 100644
--- a/tests/lean/macroStack.lean.expected.out
+++ b/tests/lean/macroStack.lean.expected.out
@@ -11,6 +11,7 @@ while expanding
 macroStack.lean:11:9-11:15: error: invalid use of `(<- ...)`, must be nested inside a 'do' expression
 macroStack.lean:17:0-17:6: error: failed to synthesize
   HAdd Nat String ?m
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 with resulting expansion
   binop% HAdd.hAdd✝ (x + x✝) x✝¹
diff --git a/tests/lean/macroSwizzle.lean.expected.out b/tests/lean/macroSwizzle.lean.expected.out
index cb31d75145..22ee932872 100644
--- a/tests/lean/macroSwizzle.lean.expected.out
+++ b/tests/lean/macroSwizzle.lean.expected.out
@@ -1,5 +1,6 @@
 macroSwizzle.lean:4:7-4:23: error: failed to synthesize
   HAdd Bool String ?m
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 macroSwizzle.lean:6:7-6:10: error: application type mismatch
   Nat.succ "x"
diff --git a/tests/lean/openScoped.lean.expected.out b/tests/lean/openScoped.lean.expected.out
index 529a44c3d9..3cb2614b34 100644
--- a/tests/lean/openScoped.lean.expected.out
+++ b/tests/lean/openScoped.lean.expected.out
@@ -1,6 +1,7 @@
 openScoped.lean:1:7-1:14: error: unknown identifier 'epsilon'
 openScoped.lean:4:2-4:24: error: failed to synthesize
   Decidable (f = g)
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 Classical.epsilon.{u} {α : Sort u} [h : Nonempty α] (p : α → Prop) : α
 openScoped.lean:15:7-15:14: error: unknown identifier 'epsilon'
diff --git a/tests/lean/prvCtor.lean.expected.out b/tests/lean/prvCtor.lean.expected.out
index e191eded00..ceeda39963 100644
--- a/tests/lean/prvCtor.lean.expected.out
+++ b/tests/lean/prvCtor.lean.expected.out
@@ -4,6 +4,7 @@ prvCtor.lean:27:7-27:8: error: unknown identifier 'a'
 prvCtor.lean:29:25-29:27: error: overloaded, errors 
   failed to synthesize
     EmptyCollection (Name "hello")
+  
   Additional diagnostic information may be available using the `set_option diagnostics true` command.
   
   invalid {...} notation, constructor for `Name` is marked as private
diff --git a/tests/lean/run/1163.lean b/tests/lean/run/1163.lean
index 7615d703a2..30e4e8f46e 100644
--- a/tests/lean/run/1163.lean
+++ b/tests/lean/run/1163.lean
@@ -16,6 +16,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
   Bool
 due to the absence of the instance above
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
@@ -29,6 +30,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
   Bool
 due to the absence of the instance above
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
diff --git a/tests/lean/run/345.lean b/tests/lean/run/345.lean
index 2a887e9c2d..c109666af0 100644
--- a/tests/lean/run/345.lean
+++ b/tests/lean/run/345.lean
@@ -6,6 +6,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Sort _
 due to the absence of the instance above
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
@@ -17,6 +18,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Sort _
 due to the absence of the instance above
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
@@ -29,6 +31,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Sort _
 due to the absence of the instance above
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
diff --git a/tests/lean/run/3554.lean b/tests/lean/run/3554.lean
index fe545a79ec..c38364fb40 100644
--- a/tests/lean/run/3554.lean
+++ b/tests/lean/run/3554.lean
@@ -6,6 +6,7 @@ set_option debug.moduleNameAtTimeout false
 /--
 error: (deterministic) timeout, maximum number of heartbeats (100) has been reached
 Use `set_option maxHeartbeats <num>` to set the limit.
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
diff --git a/tests/lean/run/3996.lean b/tests/lean/run/3996.lean
index 71af507e51..36d4441ba2 100644
--- a/tests/lean/run/3996.lean
+++ b/tests/lean/run/3996.lean
@@ -17,6 +17,7 @@ instance instB10000 : B 10000 where
 /--
 error: failed to synthesize
   A
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
diff --git a/tests/lean/run/4203.lean b/tests/lean/run/4203.lean
index 8816a0e2bc..78f50b8b96 100644
--- a/tests/lean/run/4203.lean
+++ b/tests/lean/run/4203.lean
@@ -14,6 +14,7 @@ def IsGood [DecidableEq dOut] [DecidableEq dOut₂] (Λ : Mappish dIn dOut) (Λ
 /--
 error: failed to synthesize
   Fintype v
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
diff --git a/tests/lean/run/4365.lean b/tests/lean/run/4365.lean
index bc30899d06..7635b61b1f 100644
--- a/tests/lean/run/4365.lean
+++ b/tests/lean/run/4365.lean
@@ -37,6 +37,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   String
 due to the absence of the instance above
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
@@ -48,6 +49,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Bool
 due to the absence of the instance above
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
@@ -59,6 +61,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Bool → Nat
 due to the absence of the instance above
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
@@ -70,6 +73,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
   String
 due to the absence of the instance above
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
diff --git a/tests/lean/run/by_cases.lean b/tests/lean/run/by_cases.lean
index ba75bcd62b..baf1736f86 100644
--- a/tests/lean/run/by_cases.lean
+++ b/tests/lean/run/by_cases.lean
@@ -13,6 +13,7 @@ example (p : Prop) : True := by
 /--
 error: failed to synthesize
   Decidable p
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
diff --git a/tests/lean/run/diagnosticsMsgOptional.lean b/tests/lean/run/diagnosticsMsgOptional.lean
index c9ae1886af..57335d96d6 100644
--- a/tests/lean/run/diagnosticsMsgOptional.lean
+++ b/tests/lean/run/diagnosticsMsgOptional.lean
@@ -5,6 +5,7 @@
 /--
 error: failed to synthesize
   Coe Nat Int
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
diff --git a/tests/lean/run/guard_msgs.lean b/tests/lean/run/guard_msgs.lean
index 441b41250b..156e6414cf 100644
--- a/tests/lean/run/guard_msgs.lean
+++ b/tests/lean/run/guard_msgs.lean
@@ -51,6 +51,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `22` cannot be used in a context where the expected type is
   α
 due to the absence of the instance above
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs(error) in
diff --git a/tests/lean/run/isDefEqProjIssue.lean b/tests/lean/run/isDefEqProjIssue.lean
index a972c86947..12f9b462ca 100644
--- a/tests/lean/run/isDefEqProjIssue.lean
+++ b/tests/lean/run/isDefEqProjIssue.lean
@@ -53,6 +53,7 @@ where
 /--
 error: (deterministic) timeout at `whnf`, maximum number of heartbeats (400) has been reached
 Use `set_option maxHeartbeats <num>` to set the limit.
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
diff --git a/tests/lean/run/mergeSort.lean b/tests/lean/run/mergeSort.lean
index 2215f56327..816b5f913a 100644
--- a/tests/lean/run/mergeSort.lean
+++ b/tests/lean/run/mergeSort.lean
@@ -41,6 +41,7 @@ error: could not synthesize default value for parameter 'le' using tactics
 ---
 error: failed to synthesize
   LE NoLE
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
diff --git a/tests/lean/run/variable.lean b/tests/lean/run/variable.lean
index 41fe2acb08..c5d12180b2 100644
--- a/tests/lean/run/variable.lean
+++ b/tests/lean/run/variable.lean
@@ -78,6 +78,7 @@ variable [ToString α] [ToString β]
 /--
 error: failed to synthesize
   ToString α
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
@@ -88,6 +89,7 @@ theorem t8 (a : α) (b : β) : True :=
 /--
 error: failed to synthesize
   ToString β
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
@@ -98,10 +100,12 @@ theorem t9 (a : α) (b : β) : True :=
 /--
 error: failed to synthesize
   ToString α
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 ---
 error: failed to synthesize
   ToString β
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
diff --git a/tests/lean/sanitychecks.lean.expected.out b/tests/lean/sanitychecks.lean.expected.out
index 5fde792db0..d0991b8fdf 100644
--- a/tests/lean/sanitychecks.lean.expected.out
+++ b/tests/lean/sanitychecks.lean.expected.out
@@ -9,6 +9,7 @@ sanitychecks.lean:4:8-4:32: error: 'partial' theorems are not allowed, 'partial'
 sanitychecks.lean:7:7-7:31: error: 'unsafe' theorems are not allowed
 sanitychecks.lean:10:0-10:23: error: failed to synthesize
   Inhabited False
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 sanitychecks.lean:18:12-18:20: error: invalid use of 'partial', 'Foo.unsound3' is not a function
   False
diff --git a/tests/lean/scopedLocalInsts.lean.expected.out b/tests/lean/scopedLocalInsts.lean.expected.out
index 1fa532bbcc..8dec5edcfa 100644
--- a/tests/lean/scopedLocalInsts.lean.expected.out
+++ b/tests/lean/scopedLocalInsts.lean.expected.out
@@ -1,12 +1,15 @@
 scopedLocalInsts.lean:12:6-12:39: error: failed to synthesize
   ToString A
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 "A.mk 10 20"
 scopedLocalInsts.lean:21:6-21:39: error: failed to synthesize
   ToString A
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 "{ x := 10, y := 20 }"
 scopedLocalInsts.lean:32:6-32:39: error: failed to synthesize
   ToString A
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 "A.mk 10 20"
diff --git a/tests/lean/semicolonOrLinebreak.lean.expected.out b/tests/lean/semicolonOrLinebreak.lean.expected.out
index c5311fe000..f191b4f565 100644
--- a/tests/lean/semicolonOrLinebreak.lean.expected.out
+++ b/tests/lean/semicolonOrLinebreak.lean.expected.out
@@ -7,4 +7,5 @@ term has type
   Nat
 semicolonOrLinebreak.lean:20:2-20:9: error: failed to synthesize
   Singleton ?m Point
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
diff --git a/tests/lean/setLit.lean.expected.out b/tests/lean/setLit.lean.expected.out
index 442d3c3eee..6c0a05ae84 100644
--- a/tests/lean/setLit.lean.expected.out
+++ b/tests/lean/setLit.lean.expected.out
@@ -1,12 +1,14 @@
 setLit.lean:22:19-22:21: error: overloaded, errors 
   failed to synthesize
     EmptyCollection String
+  
   Additional diagnostic information may be available using the `set_option diagnostics true` command.
   
   fields missing: 'data'
 setLit.lean:24:31-24:38: error: overloaded, errors 
   failed to synthesize
     Singleton Nat String
+  
   Additional diagnostic information may be available using the `set_option diagnostics true` command.
   
   24:33 'val' is not a field of structure 'String'
diff --git a/tests/lean/tcloop.lean.expected.out b/tests/lean/tcloop.lean.expected.out
index 76e5b73e9f..70ec0106a3 100644
--- a/tests/lean/tcloop.lean.expected.out
+++ b/tests/lean/tcloop.lean.expected.out
@@ -2,5 +2,7 @@ tcloop.lean:14:2-14:15: error: failed to synthesize
   B Nat
 (deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached
 Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
diff --git a/tests/lean/typeOf.lean.expected.out b/tests/lean/typeOf.lean.expected.out
index 2eae46dce7..5948e5926f 100644
--- a/tests/lean/typeOf.lean.expected.out
+++ b/tests/lean/typeOf.lean.expected.out
@@ -1,8 +1,10 @@
 typeOf.lean:11:22-11:25: error: failed to synthesize
   HAdd Nat Nat Bool
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 typeOf.lean:12:0-12:5: error: failed to synthesize
   HAdd Bool Nat Nat
+
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 typeOf.lean:20:56-20:62: error: invalid reassignment, term has type
   Bool : Type