diff --git a/src/Lean/Meta/Tactic/CasesOnStuckLHS.lean b/src/Lean/Meta/Tactic/CasesOnStuckLHS.lean
index d5ab94a34fb4..766bce9aa849 100644
--- a/src/Lean/Meta/Tactic/CasesOnStuckLHS.lean
+++ b/src/Lean/Meta/Tactic/CasesOnStuckLHS.lean
@@ -25,7 +25,7 @@ public partial def casesOnStuckLHS (mvarId : MVarId) : MetaM (Array MVarId) := d
   if let some (_, lhs) ← matchEqHEqLHS? target then
     if let some fvarId ← findFVar? lhs then
       return (←  mvarId.cases fvarId).map fun s => s.mvarId
-  throwError "'casesOnStuckLHS' failed"
+  throwError "`casesOnStuckLHS` failed"
 where
   findFVar? (e : Expr) : MetaM (Option FVarId) := do
     match e.getAppFn with
diff --git a/src/Lean/Meta/Tactic/Grind/Util.lean b/src/Lean/Meta/Tactic/Grind/Util.lean
index d93eba35cffb..fd87d0061b32 100644
--- a/src/Lean/Meta/Tactic/Grind/Util.lean
+++ b/src/Lean/Meta/Tactic/Grind/Util.lean
@@ -173,7 +173,7 @@ def foldProjs (e : Expr) : MetaM Expr := do
       In the test `grind_cat.lean`, the following operation fails if we are not using default
       transparency. We get the following error.
       ```
-      error: AppBuilder for 'mkProjection', structure expected
+      error: AppBuilder for `mkProjection`, structure expected
         T
       has type
         F ⟶ G
diff --git a/src/Lean/Meta/Tactic/Rewrite.lean b/src/Lean/Meta/Tactic/Rewrite.lean
index 01f7ac8cb9bb..cd84e321256d 100644
--- a/src/Lean/Meta/Tactic/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Rewrite.lean
@@ -66,10 +66,10 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
               Third, we observe that '{.ofConstName ``congrArg}' implies that 'm a = m b', which can be used with lemmas such as '{.ofConstName ``Eq.mpr}' to change the goal. \
               However, if 'e' depends on specific properties of 'a', then the motive 'm' might not typecheck.\
               \n\n\
-              Possible solutions: use rewrite's 'occs' configuration option to limit which occurrences are rewritten, \
-              or use 'simp' or 'conv' mode, which have strategies for certain kinds of dependencies \
-              (these tactics can handle proofs and '{.ofConstName ``Decidable}' instances whose types depend on the rewritten term, \
-              and 'simp' can apply user-defined '@[congr]' theorems as well)."
+              Possible solutions: use rewrite's `occs` configuration option to limit which occurrences are rewritten, \
+              or use `simp` or `conv` mode, which have strategies for certain kinds of dependencies \
+              (these tactics can handle proofs and `{.ofConstName ``Decidable}` instances whose types depend on the rewritten term, \
+              and `simp` can apply user-defined `@[congr]` theorems as well)."
           unless (← withLocalDeclD `_a α fun a => do isDefEq (← inferType (eAbst.instantiate1 a)) eType) do
             -- NB: using motive.arrow? would disallow motives where the dependency
             -- can be reduced away
diff --git a/tests/lean/motiveNotTypeCorrect.lean.expected.out b/tests/lean/motiveNotTypeCorrect.lean.expected.out
index 61e4e0bfb65a..b4d0ba9770bd 100644
--- a/tests/lean/motiveNotTypeCorrect.lean.expected.out
+++ b/tests/lean/motiveNotTypeCorrect.lean.expected.out
@@ -11,7 +11,7 @@ in the application
 
 Explanation: The rewrite tactic rewrites an expression 'e' using an equality 'a = b' by the following process. First, it looks for all 'a' in 'e'. Second, it tries to abstract these occurrences of 'a' to create a function 'm := fun _a => ...', called the *motive*, with the property that 'm a' is definitionally equal to 'e'. Third, we observe that 'congrArg' implies that 'm a = m b', which can be used with lemmas such as 'Eq.mpr' to change the goal. However, if 'e' depends on specific properties of 'a', then the motive 'm' might not typecheck.
 
-Possible solutions: use rewrite's 'occs' configuration option to limit which occurrences are rewritten, or use 'simp' or 'conv' mode, which have strategies for certain kinds of dependencies (these tactics can handle proofs and 'Decidable' instances whose types depend on the rewritten term, and 'simp' can apply user-defined '@[congr]' theorems as well).
+Possible solutions: use rewrite's `occs` configuration option to limit which occurrences are rewritten, or use `simp` or `conv` mode, which have strategies for certain kinds of dependencies (these tactics can handle proofs and `Decidable` instances whose types depend on the rewritten term, and `simp` can apply user-defined `@[congr]` theorems as well).
 
 t : Nat
 f : Nat → Nat