Tweak backticks

Author: grunweg

Mathlib/Tactic/Push.lean

@@ -197,7 +197,7 @@ def elabHead (stx : Term) : TermElabM Head := withRef stx do
   | _ =>
     match ← resolvePushId? stx with
     | some (.const c _) => return .const c
-    | _ => throwError "Could not resolve `push` argument {stx}. \
+    | _ => throwError "Could not resolve `push` argument `{stx}`. \
       Expected either a constant, e.g. `push Not`, \
       or notation with underscores, e.g. `push ¬ _`"
 
@@ -211,7 +211,7 @@ def elabDischarger (stx : TSyntax ``discharger) : TacticM Simp.Discharge :=
 def push (cfg : Config) (disch? : Option Simp.Discharge) (head : Head) (loc : Location)
     (ifUnchanged : BehaviorIfUnchanged := .error) : TacticM Unit := do
   let cfg := { distrib := cfg.distrib || (← getBoolOption `push_neg.use_distrib) }
-  transformAtLocation (pushCore head cfg disch? ·) "`push`" loc ifUnchanged
+  transformAtLocation (pushCore head cfg disch? ·) "push" loc ifUnchanged
 
 /--
 `push c` rewrites the goal by pushing the constant `c` deeper into an expression.