fix: unresolve name avoiding locals (#4593)

Fixes #4591. The extra code already existed in the only other user of
`unresolveNameGlobal` (in the pretty printer), although I did not make
it use this function because it has some additional behavior around
universes and in pattern position.

src/Lean/Elab/Tactic/Simp.lean

@@ -347,7 +347,7 @@ def mkSimpOnly (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Syntax := do
       if env.contains declName
          && (inv || !simpOnlyBuiltins.contains declName)
          && !Match.isMatchEqnTheorem env declName then
-        let decl : Term ← `($(mkIdent (← unresolveNameGlobal declName)):ident)
+        let decl : Term ← `($(mkIdent (← unresolveNameGlobalAvoidingLocals declName)):ident)
         let arg ← match post, inv with
           | true,  true  => `(Parser.Tactic.simpLemma| ← $decl:term)
           | true,  false => `(Parser.Tactic.simpLemma| $decl:term)

src/Lean/ResolveName.lean

@@ -425,4 +425,15 @@ where
           return some candidate
     return none
 
+def unresolveNameGlobalAvoidingLocals [Monad m] [MonadResolveName m] [MonadEnv m] [MonadLCtx m]
+    (n₀ : Name) (fullNames := false) : m Name := do
+  let mut n ← unresolveNameGlobal n₀ fullNames
+  unless (← getLCtx).usesUserName n do return n
+  -- `n` is also a local declaration
+  if n == n₀ then
+    -- `n` is the fully qualified name. So, we append the `_root_` prefix
+    return `_root_ ++ n
+  else
+    return n₀
+
 end Lean

tests/lean/4591.lean

@@ -0,0 +1,7 @@
+def Nat.foo : Nat → Nat
+  | 0 => 0
+  | n+1 => foo n
+decreasing_by decreasing_tactic
+
+theorem Nat.Bar.foo : foo 2 = 0 := by
+  simp? [Nat.foo]

tests/lean/4591.lean.expected.out

@@ -0,0 +1 @@
+Try this: simp only [Nat.foo]