diff --git a/src/Lean/Meta/Tactic/Assert.lean b/src/Lean/Meta/Tactic/Assert.lean
index edc80dc0b5..327c2340a8 100644
--- a/src/Lean/Meta/Tactic/Assert.lean
+++ b/src/Lean/Meta/Tactic/Assert.lean
@@ -34,5 +34,21 @@ withMVarContext mvarId $ do
   assignExprMVar mvarId newMVar;
   pure newMVar.mvarId!
 
+/--
+  Convert the given goal `Ctx |- target` into `Ctx |- forall (name : type) -> name = val -> target`.
+  It assumes `val` has type `type` -/
+def assertExt (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) (hName : Name := `h) : MetaM MVarId := do
+withMVarContext mvarId $ do
+  checkNotAssigned mvarId `assert;
+  tag    ← getMVarTag mvarId;
+  target ← getMVarType mvarId;
+  u ← getLevel type;
+  let hType := mkApp3 (mkConst `Eq [u]) type (mkBVar 0) val;
+  let newType := Lean.mkForall name BinderInfo.default type $ Lean.mkForall hName BinderInfo.default hType target;
+  newMVar ← mkFreshExprSyntheticOpaqueMVar newType tag;
+  rflPrf ← mkEqRefl val;
+  assignExprMVar mvarId (mkApp2 newMVar val rflPrf);
+  pure newMVar.mvarId!
+
 end Meta
 end Lean