From 1ed2ee4df88e4713c26968dc95539061be06fe85 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 20 Feb 2021 14:29:15 -0800
Subject: [PATCH] fix: local `simp` lemmas with implicits

---
 src/Lean/Elab/Tactic/Simp.lean   | 18 +++++++++++-------
 tests/lean/run/simpImpLocal.lean |  7 +++++++
 2 files changed, 18 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/run/simpImpLocal.lean

diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index 66ed78dc85..3670ebdedc 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/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
diff --git a/tests/lean/run/simpImpLocal.lean b/tests/lean/run/simpImpLocal.lean
new file mode 100644
index 0000000000..ae3d91eb45
--- /dev/null
+++ b/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]