diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index 2ac1d6ee68..9a8315021a 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -38,14 +38,18 @@ def elabSimpConfig (optConfig : Syntax) (ctx : Bool) : TermElabM Meta.Simp.Confi
       else
         evalSimpConfig (← instantiateMVars c)
 
-private def elabSimpLemmaTerm (stx : Syntax) : TacticM Expr := do
-  withRef stx <| Term.withoutErrToSorry do
+private def elabSimpLemmaProof (stx : Syntax) : TermElabM SimpLemma.Proof := do
+  Term.withoutModifyingElabMetaState <| withRef stx <| Term.withoutErrToSorry do
     let e ← Term.elabTerm stx none
     Term.synthesizeSyntheticMVarsUsingDefault
     let e ← instantiateMVars e
-    return e.eta
+    let e := e.eta
+    if e.hasMVar then
+      return SimpLemma.Proof.abst (← abstractMVars e)
+    else
+      return SimpLemma.Proof.expr e
 
-private def addLemma (lemmas : Meta.SimpLemmas) (e : Expr) (post : Bool): MetaM Meta.SimpLemmas := do
+private def addDeclToUnfoldOrLemma (lemmas : Meta.SimpLemmas) (e : Expr) (post : Bool): MetaM Meta.SimpLemmas := do
   if e.isConst then
     let declName := e.constName!
     let info ← getConstInfo declName
@@ -89,10 +93,8 @@ private def elabSimpLemmas (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Boo
             else
               arg[0][0].getKind == ``Parser.Tactic.simpPost
           match (← resolveSimpIdLemma? arg[1]) with
-          | some e => lemmas ← addLemma lemmas e post
-          | _ =>
-            let e ← elabSimpLemmaTerm arg[1]
-            lemmas ← addLemma lemmas e post
+          | some e => lemmas ← addDeclToUnfoldOrLemma lemmas e post
+          | _      => lemmas ← lemmas.add (← elabSimpLemmaProof arg[1]) post
       return { ctx with simpLemmas := lemmas }
 where
   resolveSimpIdLemma? (simpArgTerm : Syntax) : TacticM (Option Expr) := do
@@ -118,6 +120,7 @@ private def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (ctx := false) : Ta
 -/
 @[builtinTactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => do
   let ctx  ← mkSimpContext stx (eraseLocal := false)
+  -- trace[Meta.debug] "Lemmas {← toMessageData ctx.simpLemmas.post}"
   let loc := expandOptLocation stx[4]
   match loc with
   | Location.targets hUserNames simpTarget =>
diff --git a/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean b/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean
index a3dc41ddd1..c2f68616f5 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean
@@ -237,7 +237,8 @@ def mkSimpLemmas (proof : SimpLemma.Proof) (post : Bool := true) (prio : Nat :=
     | SimpLemma.Proof.abst _ => withIncRecDepth do
       let val ← proof.getValue
       (← preprocessProof val).mapM fun val => do
-        mkSimpLemmaCore val (SimpLemma.Proof.abst (← abstractMVars val)) post prio name?
+        let abstVal ← abstractMVars val
+        mkSimpLemmaCore abstVal.expr (SimpLemma.Proof.abst abstVal) post prio name?
 
 /- Auxiliary method for adding a local simp lemma to a `SimpLemmas` datastructure. -/
 def SimpLemmas.add (s : SimpLemmas) (proof : SimpLemma.Proof) (post : Bool := true) (prio : Nat := eval_prio default) (name? : Option Name := none): MetaM SimpLemmas := do