fix: make erased names in simp clickable (#4176)

as usually, just a matter of using the `WithInfo` variant.

Also simplifying the code a bit, it seems we can use
`realizeGlobalConstNoOverloadWithInfo` here.

(It's somehwatdubious API design that of all the functions in
the `{resolve/realise}GlobalConst{NoOverload,}{WithInfo,}` family
the one with the longest name is the one that should be used
unless one has a reason to use another one.)

Fixes: #4174

src/Lean/Elab/Tactic/Simp.lean

@@ -178,9 +178,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
             thms := thms.eraseCore (.fvar fvar.fvarId!)
           else
             let id := arg[1]
-            let declNames? ← try pure (some (← realizeGlobalConst id)) catch _ => pure none
-            if let some declNames := declNames? then
-              let declName ← ensureNonAmbiguous id declNames
+            if let .ok declName ← observing (realizeGlobalConstNoOverloadWithInfo id) then
               if (← Simp.isSimproc declName) then
                 simprocs := simprocs.erase declName
               else if ctx.config.autoUnfold then