chore: backtick identifiers in meta tactic messages

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

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

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

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