feat: improve simp local lemma elaboration

src/Lean/Elab/Tactic/Simp.lean

@@ -73,6 +73,14 @@ def elabSimpConfig (optConfig : Syntax) : TermElabM Meta.Simp.Config := do
       let c ← Term.elabTermEnsuringType optConfig[0] (Lean.mkConst ``Meta.Simp.Config)
       evalSimpConfig (← instantiateMVars c)
 
+/-- Return `some c`, if `e` is of the form `c.{?u_1, ..., ?u_n} ?m_1 ... ?m_k` -/
+private def isGlobalLemma? (e : Expr) : Option Name :=
+  e.withApp fun f args =>
+    if f.isConst && args.all (·.isMVar) && f.constLevels!.all (·.isMVar) then
+      some f.constName!
+    else
+      none
+
 /-- Elaborate extra simp lemmas provided to `simp`. `stx` is of the `simpLemma,*` -/
 private def elabSimpLemmas (stx : Syntax) (ctx : Simp.Context) : TacticM Simp.Context := do
   if stx.isNone then
@@ -92,8 +100,10 @@ private def elabSimpLemmas (stx : Syntax) (ctx : Simp.Context) : TacticM Simp.Co
             true
           else
             simpLemma[0][0].getKind == ``Parser.Tactic.simpPost
-        let term ← elabTerm simpLemma[1] none true
-        lemmas ← lemmas.add term post
+        let lemma ← elabTerm simpLemma[1] none (mayPostpone := false)
+        match isGlobalLemma? lemma with
+        | some declName => lemmas ← lemmas.addConst declName post
+        | none          => lemmas ← lemmas.add lemma post
       return { ctx with simpLemmas := lemmas }
 
 @[builtinTactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => do

src/Lean/Meta/Tactic/Simp/SimpLemmas.lean

@@ -120,6 +120,12 @@ def SimpLemmas.add (s : SimpLemmas) (e : Expr) (post : Bool := true) (prio : Nat
   let lemma ← mkSimpLemma e post prio name?
   return addSimpLemmaEntry s lemma
 
+/- Auxiliary method for adding a global declaration to a `SimpLemmas` datastructure. -/
+def SimpLemmas.addConst (s : SimpLemmas) (declName : Name) (post : Bool := true) (prio : Nat := evalPrio! default) : MetaM SimpLemmas := do
+  let cinfo ← getConstInfo declName
+  let lemma ← mkSimpLemmaCore (mkConst declName (cinfo.levelParams.map mkLevelParam)) (mkConst declName) post prio declName
+  return addSimpLemmaEntry s lemma
+
 def SimpLemma.getValue (lemma : SimpLemma) : MetaM Expr := do
   match lemma.val with
   | Expr.const declName [] _ =>

tests/lean/run/simp5.lean

@@ -0,0 +1,9 @@
+def f {α} (a b : α) := a
+
+theorem f_Eq {α} (a b : α) : f a b = a :=
+  rfl
+
+theorem ex (a b c : α) : f (f a b) c = a := by
+  simp [f_Eq]
+
+#print ex