feat(push): error message tweaks (#38008)

- make free variables in all errors "made no progress" hoverable (this applies also to ring, abel, field_simp, ...)
- include the constant being pushed in the error message

Author: grunweg

Mathlib/Tactic/Push.lean

@@ -211,7 +211,7 @@ def elabDischarger (stx : TSyntax ``discharger) : TacticM Simp.Discharge :=
 def push (cfg : Config) (disch? : Option Simp.Discharge) (head : Head) (loc : Location)
     (failIfUnchanged : Bool := true) : TacticM Unit := do
   let cfg := { distrib := cfg.distrib || (← getBoolOption `push_neg.use_distrib) }
-  transformAtLocation (pushCore head cfg disch? ·) "push" loc failIfUnchanged
+  transformAtLocation (pushCore head cfg disch? ·) s!"push {head}" loc failIfUnchanged
 
 /--
 `push c` rewrites the goal by pushing the constant `c` deeper into an expression.

Mathlib/Util/AtLocation.lean

@@ -80,15 +80,15 @@ def transformAtLocalDecl (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (
     ReaderT Simp.Context MetaM (Option MVarId) := do
   let ldecl ← fvarId.getDecl
   if ldecl.isImplementationDetail then
-    throwError "Cannot run `{proc}` at `{ldecl.userName}`, it is an implementation detail"
+    throwError "Cannot run `{proc}` at `{Expr.fvar fvarId}`, it is an implementation detail"
   let tgt ← instantiateMVars (← fvarId.getType)
   let eraseFVarId (ctx : Simp.Context) :=
     ctx.setSimpTheorems <| ctx.simpTheorems.eraseTheorem (.fvar fvarId)
   let r ← withReader eraseFVarId <| m tgt
   -- we use expression equality here (rather than defeq) to be consistent with, e.g.,
   -- `applySimpResultToLocalDeclCore`
   if failIfUnchanged && tgt.cleanupAnnotations == r.expr.cleanupAnnotations then
-    throwError "`{proc}` made no progress at `{ldecl.userName}`"
+    throwError "`{proc}` made no progress at `{Expr.fvar fvarId}`"
   return (← applySimpResultToLocalDecl goal fvarId r mayCloseGoal).map Prod.snd
 
 /-- Use the procedure `m` to transform at specified locations (hypotheses and/or goal).

MathlibTest/push_neg.lean

@@ -145,25 +145,29 @@ example (h : p ∧ q) : ¬¬(p ∧ q) := by
   exact h
 
 -- new error message as of https://github.com/leanprover-community/mathlib4/issues/27562
-/-- error: `push` made no progress anywhere -/
+/-- error: `push Not` made no progress anywhere -/
 #guard_msgs in
 example {P : Prop} (h : P) : P := by push Not at *
 
 -- new behaviour as of https://github.com/leanprover-community/mathlib4/issues/27562
 -- (Previously, because of a metavariable instantiation issue, the tactic succeeded as a no-op.)
-/-- error: `push` made no progress at `h` -/
+/-- error: `push Not` made no progress at `h` -/
 #guard_msgs in
 example {x y : ℕ} : True := by
   have h : x ≤ y := test_sorry
   push Not at h
 
 -- new behaviour as of https://github.com/leanprover-community/mathlib4/issues/27562 (previously the tactic succeeded as a no-op)
-/-- error: Cannot run `push` at `inductive_proof`, it is an implementation detail -/
+/-- error: Cannot run `push Not` at `inductive_proof`, it is an implementation detail -/
 #guard_msgs in
 def inductive_proof : True := by
   push Not at inductive_proof
   trivial
 
+/-- error: `push Not` made no progress on the goal -/
+#guard_msgs in
+example {P : Prop} (h : P) : P := by push Not
+
 section use_distrib
 
 example (h : ¬ p ∨ ¬ q) : ¬ (p ∧ q) := by