diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 98e84d86c87b..ec69b21b802d 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -620,6 +620,22 @@ def instantiateMVarsCore (mctx : MetavarContext) (e : Expr) : Expr × MetavarCon
     instantiateExprMVars e
   runST fun _ => instantiate e |>.run |>.run mctx
 
+/-
+Substitutes assigned metavariables in `e` with their assigned value according to the
+`MetavarContext`, recursively.
+
+Example:
+```
+run_meta do
+  let mvar1 ← mkFreshExprMVar (mkConst `Nat)
+  let e := (mkConst `Nat.succ).app mvar1
+  -- e is `Nat.succ ?m.773`, `?m.773` is unassigned
+  mvar1.mvarId!.assign (mkNatLit 42)
+  -- e is `Nat.succ ?m.773`, `?m.773` is assigned to `42`
+  let e' ← instantiateMVars e
+  -- e' is `Nat.succ 42`, `?m.773` is assigned to `42`
+```
+-/
 def instantiateMVars [Monad m] [MonadMCtx m] (e : Expr) : m Expr := do
   if !e.hasMVar then
     return e