diff --git a/src/Lean/ErrorExplanations/CtorResultingTypeMismatch.lean b/src/Lean/ErrorExplanations/CtorResultingTypeMismatch.lean
index 90b237b5ce..f8efa31610 100644
--- a/src/Lean/ErrorExplanations/CtorResultingTypeMismatch.lean
+++ b/src/Lean/ErrorExplanations/CtorResultingTypeMismatch.lean
@@ -27,10 +27,10 @@ inductive Tree (α : Type) where
   | node : α → Tree α → Treee α
 ```
 ```output
-Unexpected resulting type for constructor 'Tree.node': Expected an application of
+Unexpected resulting type for constructor `Tree.node`: Expected an application of
   Tree
 but found
-  ?m.22
+  ?m.2
 ```
 ```lean fixed
 inductive Tree (α : Type) where
@@ -46,7 +46,7 @@ inductive Credential where
   | password : String
 ```
 ```output
-Unexpected resulting type for constructor 'Credential.pin': Expected
+Unexpected resulting type for constructor `Credential.pin`: Expected
   Credential
 but found
   Nat
diff --git a/src/Lean/ErrorExplanations/DependsOnNoncomputable.lean b/src/Lean/ErrorExplanations/DependsOnNoncomputable.lean
index c246d76b87..90d070803a 100644
--- a/src/Lean/ErrorExplanations/DependsOnNoncomputable.lean
+++ b/src/Lean/ErrorExplanations/DependsOnNoncomputable.lean
@@ -36,7 +36,7 @@ def transformIfZero : Nat → Nat
   | n => n
 ```
 ```output
-axiom 'transform' not supported by code generator; consider marking definition as 'noncomputable'
+`transform` not supported by code generator; consider marking definition as `noncomputable`
 ```
 ```lean fixed
 axiom transform : Nat → Nat
@@ -63,7 +63,7 @@ def endsOrDefault (ns : List Nat) : Nat × Nat :=
   (head, tail)
 ```
 ```output
-failed to compile definition, consider marking it as 'noncomputable' because it depends on 'getOrDefault', which is 'noncomputable'
+failed to compile definition, consider marking it as 'noncomputable' because it depends on 'propDecidable', which is 'noncomputable'
 ```
 ```lean fixed (title := "Fixed (computable)")
 def getOrDefault [Inhabited α] : Option α → α
diff --git a/src/Lean/ErrorExplanations/InductiveParamMismatch.lean b/src/Lean/ErrorExplanations/InductiveParamMismatch.lean
index a081157fcb..bcf273751b 100644
--- a/src/Lean/ErrorExplanations/InductiveParamMismatch.lean
+++ b/src/Lean/ErrorExplanations/InductiveParamMismatch.lean
@@ -41,7 +41,7 @@ The provided argument
 is not definitionally equal to the expected parameter
   n
 
-Note: The value of parameter 'n' must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.
+Note: The value of parameter `n` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.
 ```
 ```lean fixed
 inductive Vec (α : Type) : Nat → Type where
diff --git a/src/Lean/ErrorExplanations/PropRecLargeElim.lean b/src/Lean/ErrorExplanations/PropRecLargeElim.lean
index 01ec7fd9c4..45e953f2bb 100644
--- a/src/Lean/ErrorExplanations/PropRecLargeElim.lean
+++ b/src/Lean/ErrorExplanations/PropRecLargeElim.lean
@@ -44,7 +44,7 @@ Tactic `cases` failed with a nested error:
 Tactic `induction` failed: recursor `Nonempty.casesOn` can only eliminate into `Prop`
 
 α : Type
-motive : Nonempty α → Sort ?u.1416
+motive : Nonempty α → Sort ?u.52
 h_1 : (x : α) → motive ⋯
 inst✝ : Nonempty α
 ⊢ motive inst✝
@@ -81,7 +81,7 @@ Tactic `induction` failed: recursor `Exists.casesOn` can only eliminate into `Pr
 
 α : Type u
 p : α → Prop
-motive : (∃ x, p x) → Sort ?u.1419
+motive : (∃ x, p x) → Sort ?u.48
 h_1 : (x : α) → (h : p x) → motive ⋯
 h✝ : ∃ x, p x
 ⊢ motive h✝
diff --git a/src/Lean/ErrorExplanations/UnknownIdentifier.lean b/src/Lean/ErrorExplanations/UnknownIdentifier.lean
index 9d7b24b18b..4d76f6bd1c 100644
--- a/src/Lean/ErrorExplanations/UnknownIdentifier.lean
+++ b/src/Lean/ErrorExplanations/UnknownIdentifier.lean
@@ -42,7 +42,7 @@ def inventory :=
   Std.HashSet.ofList [("apples", 3), ("bananas", 4)]
 ```
 ```output
-Unknown constant `Std.HashSet.ofList`
+Unknown identifier `Std.HashSet.ofList`
 ```
 ```lean fixed
 public import Std.Data.HashSet.Basic
@@ -163,7 +163,7 @@ def disjoinToNat (b₁ b₂ : Bool) : Nat :=
   .toNat (b₁ || b₂)
 ```
 ```output
-Unknown identifier `Nat.toNat`
+Unknown constant `Nat.toNat`
 
 Note: Inferred this name from the expected resulting type of `.toNat`:
   Nat