diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index c559c9d732..2b0ff5806c 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -341,6 +341,13 @@ def closeMainGoal (val : Expr) (checkUnassigned := true): TacticM Unit := do
     let gs ← tactic mvarId
     pure ((), gs)
 
+@[inline] def liftMetaTactic1 (tactic : MVarId → MetaM (Option MVarId)) : TacticM Unit :=
+  withMainContext do
+    if let some mvarId ← tactic (← getMainGoal) then
+      replaceMainGoal [mvarId]
+    else
+      replaceMainGoal []
+
 def tryTactic? (tactic : TacticM α) : TacticM (Option α) := do
   try
     pure (some (← tactic))
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index e8702259de..c8c3d983c9 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -171,33 +171,17 @@ private def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (ctx := false) (ign
   -- trace[Meta.debug] "Lemmas {← toMessageData ctx.simpLemmas.post}"
   let loc := expandOptLocation stx[4]
   match loc with
-  | Location.targets hUserNames simpTarget =>
+  | Location.targets hUserNames simplifyTarget =>
     withMainContext do
       let fvarIds ← hUserNames.mapM fun hUserName => return (← getLocalDeclFromUserName hUserName).fvarId
-      go ctx fvarIds simpTarget fvarIdToLemmaId
+      go ctx fvarIds simplifyTarget fvarIdToLemmaId
   | Location.wildcard =>
     withMainContext do
-      go ctx (← getNondepPropHyps (← getMainGoal)) (simpType := true) fvarIdToLemmaId
+      go ctx (← getNondepPropHyps (← getMainGoal)) (simplifyTarget := true) fvarIdToLemmaId
 where
-  go (ctx : Simp.Context) (fvarIdsToSimp : Array FVarId) (simpType : Bool) (fvarIdToLemmaId : FVarIdToLemmaId) : TacticM Unit := do
-    let mut mvarId ← getMainGoal
-    let mut toAssert : Array Hypothesis := #[]
-    for fvarId in fvarIdsToSimp do
-      let localDecl ← getLocalDecl fvarId
-      let type ← instantiateMVars localDecl.type
-      let ctx ← match fvarIdToLemmaId.find? localDecl.fvarId with
-        | none => pure ctx
-        | some lemmaId => pure { ctx with simpLemmas := (← ctx.simpLemmas.eraseCore lemmaId) }
-      match (← simpStep mvarId (mkFVar fvarId) type ctx) with
-      | none => replaceMainGoal []; return ()
-      | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
-    if simpType then
-      match (← simpTarget mvarId ctx) with
-      | none => replaceMainGoal []; return ()
-      | some mvarIdNew => mvarId := mvarIdNew
-    let (_, mvarIdNew) ← assertHypotheses mvarId toAssert
-    let mvarIdNew ← tryClearMany mvarIdNew fvarIdsToSimp
-    replaceMainGoal [mvarIdNew]
+  go (ctx : Simp.Context) (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) (fvarIdToLemmaId : FVarIdToLemmaId) : TacticM Unit := do
+    liftMetaTactic1 fun mvarId =>
+      simpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp) (fvarIdToLemmaId := fvarIdToLemmaId)
 
 @[builtinTactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => do
   let { ctx, .. } ← mkSimpContext stx (eraseLocal := true) (ctx := true) (ignoreStarArg := true)
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 6d3da28501..b298144c54 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -414,4 +414,26 @@ def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context)
       else
         return some (proof, r.expr)
 
+abbrev FVarIdToLemmaId := NameMap Name
+
+def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) (fvarIdToLemmaId : FVarIdToLemmaId := {}) : MetaM (Option MVarId) := do
+  let mut mvarId := mvarId
+  let mut toAssert : Array Hypothesis := #[]
+  for fvarId in fvarIdsToSimp do
+    let localDecl ← getLocalDecl fvarId
+    let type ← instantiateMVars localDecl.type
+    let ctx ← match fvarIdToLemmaId.find? localDecl.fvarId with
+      | none => pure ctx
+      | some lemmaId => pure { ctx with simpLemmas := (← ctx.simpLemmas.eraseCore lemmaId) }
+    match (← simpStep mvarId (mkFVar fvarId) type ctx discharge?) with
+    | none => return none
+    | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
+  if simplifyTarget then
+    match (← simpTarget mvarId ctx discharge?) with
+    | none => return none
+    | some mvarIdNew => mvarId := mvarIdNew
+  let (_, mvarIdNew) ← assertHypotheses mvarId toAssert
+  let mvarIdNew ← tryClearMany mvarIdNew fvarIdsToSimp
+  return mvarIdNew
+
 end Lean.Meta