fix: local simp lemmas with implicits

src/Lean/Elab/Tactic/Simp.lean

@@ -94,21 +94,25 @@ private def elabSimpLemmas (stx : Syntax) (ctx : Simp.Context) : TacticM Simp.Co
           else
             arg[0][0].getKind == ``Parser.Tactic.simpPost
         match (← resolveSimpIdLemma? arg[1]) with
-        | some declName =>
-          let info ← getConstInfo declName
-          if (← isProp info.type) then
-            lemmas ← lemmas.addConst declName post
+        | some e =>
+          if e.isConst then
+            let declName := e.constName!
+            let info ← getConstInfo declName
+            if (← isProp info.type) then
+              lemmas ← lemmas.addConst declName post
+            else
+              toUnfold := toUnfold.insert declName
           else
-            toUnfold := toUnfold.insert declName
+            lemmas ← lemmas.add e post
         | _ =>
           let arg ← elabTerm arg[1] none (mayPostpone := false)
           lemmas ← lemmas.add arg post
       return { ctx with simpLemmas := lemmas, toUnfold := toUnfold }
 where
-  resolveSimpIdLemma? (simpArgTerm : Syntax) : TacticM (Option Name) := do
+  resolveSimpIdLemma? (simpArgTerm : Syntax) : TacticM (Option Expr) := do
     if simpArgTerm.isIdent then
       try
-        return some (← resolveGlobalConstNoOverload simpArgTerm.getId)
+        Term.resolveId? simpArgTerm
       catch _ =>
         return none
     else

tests/lean/run/simpImpLocal.lean

@@ -0,0 +1,7 @@
+theorem ex [Add α]
+            (assoc : {a b c : α} → a + b + c = a + (b + c))
+            (comm  : {a b : α} → a + b = b + a)
+            (f : α → α) (x y z : α) : f (x + (y + z)) = f (y + (x + z)) := by
+  let leftAssoc {a b c : α} : a + (b + c) = b + (a + c) := by
+    rw [← assoc, comm (a := a), assoc]
+  simp [leftAssoc]