diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index b76a26f481..9c217e9ef8 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -340,5 +340,9 @@ u ← getDecLevel `mkArrayLit type;
 listLit ← mkListLit type xs;
 pure (mkApp (mkApp (mkConst `List.toArray [u]) type) listLit)
 
+def mkSorry (type : Expr) (synthetic : Bool) : MetaM Expr := do
+u ← getLevel type;
+pure $ mkApp2 (mkConst `sorryAx [u]) type (toExpr synthetic)
+
 end Meta
 end Lean
diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean
index 5cdb9f4b9c..55637b4937 100644
--- a/src/Lean/Meta/Tactic/Util.lean
+++ b/src/Lean/Meta/Tactic/Util.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Meta.Basic
+import Lean.Meta.AppBuilder
 import Lean.Meta.LevelDefEq
 
 namespace Lean
@@ -44,5 +45,14 @@ instance Meta.hasOrelse {α} : HasOrelse (MetaM α) := ⟨Meta.orelse⟩
 @[init] private def regTraceClasses : IO Unit :=
 registerTraceClass `Meta.Tactic
 
+/-- Assign `mvarId` to `sorryAx` -/
+def admit (mvarId : MVarId) (synthetic := true) : MetaM Unit :=
+withMVarContext mvarId $ do
+  checkNotAssigned mvarId `admit;
+  mvarType ← getMVarType mvarId;
+  val ← mkSorry mvarType synthetic;
+  assignExprMVar mvarId val;
+  pure ()
+
 end Meta
 end Lean