diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 75eae9b8ad..0e79af6a73 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -31,7 +31,16 @@ register_builtin_option maxHeartbeats : Nat := {
   descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
 }
 
-def useDiagnosticMsg := s!"use `set_option {diagnostics.name} true` to get diagnostic information"
+/--
+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}"`.
+-/
+def useDiagnosticMsg : MessageData :=
+  MessageData.lazy fun ctx =>
+    if diagnostics.get ctx.opts then
+      pure ""
+    else
+      pure s!"\nAdditional diagnostic information may be available by using the `set_option {diagnostics.name} true` command."
 
 namespace Core
 
@@ -300,8 +309,10 @@ register_builtin_option debug.moduleNameAtTimeout : Bool := {
 def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
   let includeModuleName := debug.moduleNameAtTimeout.get (← getOptions)
   let atModuleName := if includeModuleName then s!" at `{moduleName}`" else ""
-  let msg := s!"(deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\nuse `set_option {optionName} <num>` to set the limit\n{useDiagnosticMsg}"
-  throw <| Exception.error (← getRef) (MessageData.ofFormat (Std.Format.text msg))
+  throw <| Exception.error (← getRef) m!"\
+    (deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\n\
+    Use `set_option {optionName} <num>` to set the limit.\
+    {useDiagnosticMsg}"
 
 def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat) : CoreM Unit := do
   unless max == 0 do
diff --git a/src/Lean/Elab/Calc.lean b/src/Lean/Elab/Calc.lean
index fa4d275895..d5586da4db 100644
--- a/src/Lean/Elab/Calc.lean
+++ b/src/Lean/Elab/Calc.lean
@@ -42,7 +42,7 @@ def mkCalcTrans (result resultType step stepType : Expr) : MetaM (Expr × Expr)
     unless (← getCalcRelation? resultType).isSome do
       throwError "invalid 'calc' step, step result is not a relation{indentExpr resultType}"
     return (result, resultType)
-  | _ => throwError "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}\n{useDiagnosticMsg}"
+  | _ => throwError "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}{useDiagnosticMsg}"
 
 /--
 Adds a type annotation to a hole that occurs immediately at the beginning of the term.
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 3d4c4c7623..ea14af6e70 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -996,7 +996,7 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
     if (← read).ignoreTCFailures then
       return false
     else
-      throwError "failed to synthesize{indentExpr type}{extraErrorMsg}\n{useDiagnosticMsg}"
+      throwError "failed to synthesize{indentExpr type}{extraErrorMsg}{useDiagnosticMsg}"
 
 def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
   withTraceNode `Elab.coe (fun _ => return m!"adding coercion for {e} : {← inferType e} =?= {expectedType}") do
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index afd5129422..e412bfe451 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -636,7 +636,7 @@ def main (type : Expr) (maxResultSize : Nat) : MetaM (Option AbstractMVarsResult
        (action.run { maxResultSize := maxResultSize, maxHeartbeats := getMaxHeartbeats (← getOptions) } |>.run' {})
        fun ex =>
          if ex.isRuntime then
-           throwError "failed to synthesize{indentExpr type}\n{ex.toMessageData}\n{useDiagnosticMsg}"
+           throwError "failed to synthesize{indentExpr type}\n{ex.toMessageData}{useDiagnosticMsg}"
          else
            throw ex
 
@@ -810,7 +810,7 @@ def trySynthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM
     (fun _ => pure LOption.undef)
 
 def throwFailedToSynthesize (type : Expr) : MetaM Expr :=
-  throwError "failed to synthesize{indentExpr type}\n{useDiagnosticMsg}"
+  throwError "failed to synthesize{indentExpr type}{useDiagnosticMsg}"
 
 def synthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM Expr :=
   catchInternalId isDefEqStuckExceptionId
diff --git a/tests/lean/1007.lean.expected.out b/tests/lean/1007.lean.expected.out
index 535431abf0..f947d152d2 100644
--- a/tests/lean/1007.lean.expected.out
+++ b/tests/lean/1007.lean.expected.out
@@ -8,4 +8,4 @@
 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
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
diff --git a/tests/lean/1102.lean.expected.out b/tests/lean/1102.lean.expected.out
index d94f2b5cb6..127e652fdb 100644
--- a/tests/lean/1102.lean.expected.out
+++ b/tests/lean/1102.lean.expected.out
@@ -1,3 +1,3 @@
 1102.lean:22:35-22:49: error: failed to synthesize
   DVR 1
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
diff --git a/tests/lean/2040.lean.expected.out b/tests/lean/2040.lean.expected.out
index 9cf0cfb86e..9788138631 100644
--- a/tests/lean/2040.lean.expected.out
+++ b/tests/lean/2040.lean.expected.out
@@ -1,12 +1,12 @@
 2040.lean:8:8-8:13: error: failed to synthesize
   HPow Nat Nat Int
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 2040.lean:14:8-14:13: error: failed to synthesize
   HPow Nat Nat Int
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 2040.lean:20:8-20:13: error: failed to synthesize
   HPow Nat Nat Int
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 2040.lean:18:2-20:22: error: type mismatch
   trans (sorryAx (a = 37)) (sorryAx (37 = 2 ^ n))
 has type
diff --git a/tests/lean/2220.lean.expected.out b/tests/lean/2220.lean.expected.out
index 8b03b90883..22390ad15f 100644
--- a/tests/lean/2220.lean.expected.out
+++ b/tests/lean/2220.lean.expected.out
@@ -8,11 +8,11 @@
 @HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int
 2220.lean:25:19-25:24: error: failed to synthesize
   HPow Nat Nat Int
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 @HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
   (@HPow.hPow Nat Nat Int ?m (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
 2220.lean:26:12-26:17: error: failed to synthesize
   HPow Nat Nat Int
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 @HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
   (@HPow.hPow Nat Nat Int ?m (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
diff --git a/tests/lean/2273.lean.expected.out b/tests/lean/2273.lean.expected.out
index c15377bb35..dcc0ceb92c 100644
--- a/tests/lean/2273.lean.expected.out
+++ b/tests/lean/2273.lean.expected.out
@@ -1,3 +1,3 @@
 2273.lean:9:8-9:14: error: failed to synthesize
   P 37
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
diff --git a/tests/lean/297.lean.expected.out b/tests/lean/297.lean.expected.out
index 7c265e378c..d7ca31788d 100644
--- a/tests/lean/297.lean.expected.out
+++ b/tests/lean/297.lean.expected.out
@@ -3,4 +3,4 @@
 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
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
diff --git a/tests/lean/386.lean.expected.out b/tests/lean/386.lean.expected.out
index 21c952dd87..530fa5ba18 100644
--- a/tests/lean/386.lean.expected.out
+++ b/tests/lean/386.lean.expected.out
@@ -1,3 +1,3 @@
 386.lean:9:2-9:46: error: failed to synthesize
   Fintype ?m
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
diff --git a/tests/lean/448.lean.expected.out b/tests/lean/448.lean.expected.out
index 14d369862a..ec80bfed69 100644
--- a/tests/lean/448.lean.expected.out
+++ b/tests/lean/448.lean.expected.out
@@ -1,3 +1,3 @@
 448.lean:21:2-23:20: error: failed to synthesize
   MonadExceptOf IO.Error M
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
diff --git a/tests/lean/attrCmd.lean.expected.out b/tests/lean/attrCmd.lean.expected.out
index 814c35d447..5551509eae 100644
--- a/tests/lean/attrCmd.lean.expected.out
+++ b/tests/lean/attrCmd.lean.expected.out
@@ -1,3 +1,3 @@
 attrCmd.lean:6:0-6:6: error: failed to synthesize
   Pure M
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
diff --git a/tests/lean/calcErrors.lean.expected.out b/tests/lean/calcErrors.lean.expected.out
index 2ac5779a74..85598c69c5 100644
--- a/tests/lean/calcErrors.lean.expected.out
+++ b/tests/lean/calcErrors.lean.expected.out
@@ -12,7 +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
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 calcErrors.lean:41:7-41:12: error: invalid 'calc' step, left-hand-side is
   γ : Sort u_1
 previous right-hand-side is
diff --git a/tests/lean/defInst.lean.expected.out b/tests/lean/defInst.lean.expected.out
index 8bb2e82879..4014c89f3d 100644
--- a/tests/lean/defInst.lean.expected.out
+++ b/tests/lean/defInst.lean.expected.out
@@ -1,7 +1,7 @@
 [4, 5, 6]
 defInst.lean:8:26-8:32: error: failed to synthesize
   BEq Foo
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 fun x y => sorryAx (?m x y) true : (x y : Foo) → ?m x y
 [4, 5, 6]
 fun x y => x == y : Foo → Foo → Bool
diff --git a/tests/lean/defaultInstance.lean.expected.out b/tests/lean/defaultInstance.lean.expected.out
index 8612de8a01..ce40f49119 100644
--- a/tests/lean/defaultInstance.lean.expected.out
+++ b/tests/lean/defaultInstance.lean.expected.out
@@ -1,5 +1,5 @@
 defaultInstance.lean:20:20-20:23: error: failed to synthesize
   Foo Bool (?m x)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by 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 ff3e277fa7..098500b40a 100644
--- a/tests/lean/eagerUnfoldingIssue.lean.expected.out
+++ b/tests/lean/eagerUnfoldingIssue.lean.expected.out
@@ -1,6 +1,6 @@
 eagerUnfoldingIssue.lean:6:2-6:17: error: failed to synthesize
   MonadLog (StateM Nat)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 eagerUnfoldingIssue.lean:12:2-12:17: error: failed to synthesize
   MonadLog (StateM Nat)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
diff --git a/tests/lean/eraseInsts.lean.expected.out b/tests/lean/eraseInsts.lean.expected.out
index 7fbc16acae..d4bbcf4593 100644
--- a/tests/lean/eraseInsts.lean.expected.out
+++ b/tests/lean/eraseInsts.lean.expected.out
@@ -1,3 +1,3 @@
 eraseInsts.lean:12:22-12:27: error: failed to synthesize
   HAdd Foo Foo ?m
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
diff --git a/tests/lean/forErrors.lean.expected.out b/tests/lean/forErrors.lean.expected.out
index 860344f9ea..911b25b697 100644
--- a/tests/lean/forErrors.lean.expected.out
+++ b/tests/lean/forErrors.lean.expected.out
@@ -1,3 +1,3 @@
 forErrors.lean:3:29-3:30: error: failed to synthesize
   ToStream α ?m
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
diff --git a/tests/lean/kernelMVarBug.lean.expected.out b/tests/lean/kernelMVarBug.lean.expected.out
index 19feec3023..70cd682386 100644
--- a/tests/lean/kernelMVarBug.lean.expected.out
+++ b/tests/lean/kernelMVarBug.lean.expected.out
@@ -1,3 +1,3 @@
 kernelMVarBug.lean:5:15-5:20: error: failed to synthesize
   HAdd α α α
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
diff --git a/tests/lean/macroStack.lean.expected.out b/tests/lean/macroStack.lean.expected.out
index f044792348..9cfb577c7c 100644
--- a/tests/lean/macroStack.lean.expected.out
+++ b/tests/lean/macroStack.lean.expected.out
@@ -11,7 +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
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 with resulting expansion
   binop% HAdd.hAdd✝ (x + x✝) x✝¹
 while expanding
diff --git a/tests/lean/macroSwizzle.lean.expected.out b/tests/lean/macroSwizzle.lean.expected.out
index a5f6b79cda..b250009a78 100644
--- a/tests/lean/macroSwizzle.lean.expected.out
+++ b/tests/lean/macroSwizzle.lean.expected.out
@@ -1,6 +1,6 @@
 macroSwizzle.lean:4:7-4:23: error: failed to synthesize
   HAdd Bool String ?m
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 macroSwizzle.lean:6:7-6:10: error: application type mismatch
   Nat.succ "x"
 argument
diff --git a/tests/lean/openScoped.lean.expected.out b/tests/lean/openScoped.lean.expected.out
index f2449eb935..0a23b21693 100644
--- a/tests/lean/openScoped.lean.expected.out
+++ b/tests/lean/openScoped.lean.expected.out
@@ -1,7 +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)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by 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'
 openScoped.lean:20:7-20:14: error: unknown identifier 'epsilon'
diff --git a/tests/lean/prvCtor.lean.expected.out b/tests/lean/prvCtor.lean.expected.out
index a1de1f6b0f..e3c95f1e05 100644
--- a/tests/lean/prvCtor.lean.expected.out
+++ b/tests/lean/prvCtor.lean.expected.out
@@ -7,7 +7,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")
-  use `set_option diagnostics true` to get diagnostic information
+  Additional diagnostic information may be available by using the `set_option diagnostics true` command.
   
   invalid {...} notation, constructor for `Name` is marked as private
 prvCtor.lean:31:25-31:34: error: invalid ⟨...⟩ notation, constructor for `Name` is marked as private
diff --git a/tests/lean/run/1163.lean b/tests/lean/run/1163.lean
index cdd3b44d61..26685b4548 100644
--- a/tests/lean/run/1163.lean
+++ b/tests/lean/run/1163.lean
@@ -16,7 +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
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 def x : Bool := 0
@@ -29,7 +29,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
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 theorem result4 : False := by -- Does not generate a `sorry` warning because there is an error
diff --git a/tests/lean/run/3313.lean b/tests/lean/run/3313.lean
index 1b81992add..62a5180a9c 100644
--- a/tests/lean/run/3313.lean
+++ b/tests/lean/run/3313.lean
@@ -41,7 +41,6 @@ info: [type_class] max synth pending failures (maxSynthPendingDepth: 1), use `se
 ---
 error: failed to synthesize
   HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R)))
-use `set_option diagnostics true` to get diagnostic information
 -/
 #guard_msgs in
 set_option diagnostics true in
diff --git a/tests/lean/run/345.lean b/tests/lean/run/345.lean
index fd99507518..a00bb02d27 100644
--- a/tests/lean/run/345.lean
+++ b/tests/lean/run/345.lean
@@ -6,7 +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
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 axiom bla : 1
@@ -17,7 +17,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
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 structure Foo where
@@ -29,7 +29,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
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 inductive Bla (x : 1) : Type
diff --git a/tests/lean/run/3554.lean b/tests/lean/run/3554.lean
index ac3afc8ef3..8458c60d40 100644
--- a/tests/lean/run/3554.lean
+++ b/tests/lean/run/3554.lean
@@ -5,8 +5,12 @@ def foo : Nat → Nat
 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
-use `set_option diagnostics true` to get diagnostic information
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
+---
+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 by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 set_option maxHeartbeats 100 in
diff --git a/tests/lean/run/3996.lean b/tests/lean/run/3996.lean
index cd2592851c..dba0ec5f5a 100644
--- a/tests/lean/run/3996.lean
+++ b/tests/lean/run/3996.lean
@@ -17,7 +17,7 @@ instance instB10000 : B 10000 where
 /--
 error: failed to synthesize
   A
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 #synth A -- should fail quickly
diff --git a/tests/lean/run/4203.lean b/tests/lean/run/4203.lean
index 86caf423e4..bb3fc788d9 100644
--- a/tests/lean/run/4203.lean
+++ b/tests/lean/run/4203.lean
@@ -14,7 +14,7 @@ def IsGood [DecidableEq dOut] [DecidableEq dOut₂] (Λ : Mappish dIn dOut) (Λ
 /--
 error: failed to synthesize
   Fintype v
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 def MappishOrder [DecidableEq dIn] : Preorder
diff --git a/tests/lean/run/4365.lean b/tests/lean/run/4365.lean
index 5b7207adb6..29afb1caff 100644
--- a/tests/lean/run/4365.lean
+++ b/tests/lean/run/4365.lean
@@ -37,7 +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
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 #check (1 : String)
@@ -48,7 +48,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
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 #check (1 : Bool)
@@ -59,7 +59,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
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 #check (1 : Bool → Nat)
@@ -70,7 +70,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
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 def foo : String :=
diff --git a/tests/lean/run/by_cases.lean b/tests/lean/run/by_cases.lean
index 3289c1a7ff..b76280fff7 100644
--- a/tests/lean/run/by_cases.lean
+++ b/tests/lean/run/by_cases.lean
@@ -13,7 +13,7 @@ example (p : Prop) : True := by
 /--
 error: failed to synthesize
   Decidable p
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 example (p : Prop) : True := by
diff --git a/tests/lean/run/diagnosticsMsgOptional.lean b/tests/lean/run/diagnosticsMsgOptional.lean
new file mode 100644
index 0000000000..257cfa860e
--- /dev/null
+++ b/tests/lean/run/diagnosticsMsgOptional.lean
@@ -0,0 +1,20 @@
+/-!
+# Mentioning `set_option diagnostics true` depends on it not already being set
+-/
+
+/--
+error: failed to synthesize
+  Coe Nat Int
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+#synth Coe Nat Int
+
+set_option diagnostics true
+
+/--
+error: failed to synthesize
+  Coe Nat Int
+-/
+#guard_msgs in
+#synth Coe Nat Int
diff --git a/tests/lean/run/guard_msgs.lean b/tests/lean/run/guard_msgs.lean
index 0135d4b599..c215bc5fa1 100644
--- a/tests/lean/run/guard_msgs.lean
+++ b/tests/lean/run/guard_msgs.lean
@@ -51,7 +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
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs(error) in
 example : α := 22
@@ -107,7 +107,7 @@ Lax whitespace
 /--
 error: failed to synthesize
   DecidableEq (Nat → Nat)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs (whitespace := lax) in
 #synth DecidableEq (Nat → Nat)
@@ -115,7 +115,7 @@ use `set_option diagnostics true` to get diagnostic information
 /--
 error: failed to synthesize
   DecidableEq (Nat → Nat)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs (whitespace := lax) in
 #synth DecidableEq (Nat → Nat)
diff --git a/tests/lean/run/isDefEqProjIssue.lean b/tests/lean/run/isDefEqProjIssue.lean
index de429cecdf..e71137102d 100644
--- a/tests/lean/run/isDefEqProjIssue.lean
+++ b/tests/lean/run/isDefEqProjIssue.lean
@@ -52,8 +52,36 @@ where
 
 /--
 error: (deterministic) timeout at `whnf`, maximum number of heartbeats (400) has been reached
-use `set_option maxHeartbeats <num>` to set the limit
-use `set_option diagnostics true` to get diagnostic information
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
+---
+error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
+---
+error: (deterministic) timeout at `elaborator`, maximum number of heartbeats (400) has been reached
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
+---
+error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
+---
+error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
+---
+error: (deterministic) timeout at `elaborator`, maximum number of heartbeats (400) has been reached
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
+---
+error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
+---
+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 by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 set_option backward.isDefEq.lazyWhnfCore false in
diff --git a/tests/lean/sanitychecks.lean.expected.out b/tests/lean/sanitychecks.lean.expected.out
index 3958cd21a7..67a8f2eaf0 100644
--- a/tests/lean/sanitychecks.lean.expected.out
+++ b/tests/lean/sanitychecks.lean.expected.out
@@ -9,7 +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
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by 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
 sanitychecks.lean:20:0-20:54: error: failed to compile partial definition 'Foo.unsound4', failed to show that type is inhabited and non empty
diff --git a/tests/lean/scopedLocalInsts.lean.expected.out b/tests/lean/scopedLocalInsts.lean.expected.out
index 9a3ab1cac8..d4bc1c5699 100644
--- a/tests/lean/scopedLocalInsts.lean.expected.out
+++ b/tests/lean/scopedLocalInsts.lean.expected.out
@@ -1,12 +1,12 @@
 scopedLocalInsts.lean:12:6-12:39: error: failed to synthesize
   ToString A
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 "A.mk 10 20"
 scopedLocalInsts.lean:21:6-21:39: error: failed to synthesize
   ToString A
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 "{ x := 10, y := 20 }"
 scopedLocalInsts.lean:32:6-32:39: error: failed to synthesize
   ToString A
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by 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 2383a4e139..190bbfee00 100644
--- a/tests/lean/semicolonOrLinebreak.lean.expected.out
+++ b/tests/lean/semicolonOrLinebreak.lean.expected.out
@@ -7,4 +7,4 @@ term has type
   Nat
 semicolonOrLinebreak.lean:20:2-20:9: error: failed to synthesize
   Singleton ?m Point
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
diff --git a/tests/lean/setLit.lean.expected.out b/tests/lean/setLit.lean.expected.out
index 1f63e7cc4c..c2da77acbd 100644
--- a/tests/lean/setLit.lean.expected.out
+++ b/tests/lean/setLit.lean.expected.out
@@ -1,12 +1,12 @@
 setLit.lean:22:19-22:21: error: overloaded, errors 
   failed to synthesize
     EmptyCollection String
-  use `set_option diagnostics true` to get diagnostic information
+  Additional diagnostic information may be available by 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
-  use `set_option diagnostics true` to get diagnostic information
+  Additional diagnostic information may be available by 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 4b0a694e9a..dff58ab124 100644
--- a/tests/lean/tcloop.lean.expected.out
+++ b/tests/lean/tcloop.lean.expected.out
@@ -1,6 +1,3 @@
-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
-use `set_option diagnostics true` to get diagnostic information
-use `set_option diagnostics true` to get diagnostic information
+tcloop.lean:14:2-14:15: error: (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 by using the `set_option diagnostics true` command.
diff --git a/tests/lean/typeOf.lean.expected.out b/tests/lean/typeOf.lean.expected.out
index 65329e1845..53f3810095 100644
--- a/tests/lean/typeOf.lean.expected.out
+++ b/tests/lean/typeOf.lean.expected.out
@@ -1,9 +1,9 @@
 typeOf.lean:11:22-11:25: error: failed to synthesize
   HAdd Nat Nat Bool
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 typeOf.lean:12:0-12:5: error: failed to synthesize
   HAdd Bool Nat Nat
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 typeOf.lean:20:56-20:62: error: invalid reassignment, term has type
   Bool : Type
 but is expected to have type