diff --git a/src/Init/Lean/Meta/Tactic/Apply.lean b/src/Init/Lean/Meta/Tactic/Apply.lean
index 963234c482..ffbc3d22d3 100644
--- a/src/Init/Lean/Meta/Tactic/Apply.lean
+++ b/src/Init/Lean/Meta/Tactic/Apply.lean
@@ -47,6 +47,11 @@ unless parentTag.isAnonymous $
       currTag ← getMVarTag newMVarId;
       renameMVar newMVarId (parentTag ++ currTag.eraseMacroScopes)
 
+def postprocessAppMVars (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) : MetaM Unit := do
+synthAppInstances tacticName mvarId newMVars binderInfos;
+-- TODO: default and auto params
+appendParentTag mvarId newMVars binderInfos
+
 private def dependsOnOthers (mvar : Expr) (otherMVars : Array Expr) : MetaM Bool :=
 otherMVars.anyM $ fun otherMVar =>
   if mvar == otherMVar then pure false
@@ -80,10 +85,8 @@ withMVarContext mvarId $ do
   };
   (newMVars, binderInfos, eType) ← forallMetaTelescopeReducing eType (some numArgs);
   unlessM (isDefEq eType targetType) $ throwApplyError mvarId eType targetType;
-  synthAppInstances `apply mvarId newMVars binderInfos;
-  let val := mkAppN e newMVars;
-  assignExprMVar mvarId val;
-  appendParentTag mvarId newMVars binderInfos;
+  postprocessAppMVars `apply mvarId newMVars binderInfos;
+  assignExprMVar mvarId (mkAppN e newMVars);
   newMVars ← newMVars.filterM $ fun mvar => not <$> isExprMVarAssigned mvar.mvarId!;
   -- TODO: add option `ApplyNewGoals` and implement other orders
   reorderNonDependentFirst newMVars
diff --git a/src/Init/Lean/Meta/Tactic/Assert.lean b/src/Init/Lean/Meta/Tactic/Assert.lean
index 468341928f..90f04d2182 100644
--- a/src/Init/Lean/Meta/Tactic/Assert.lean
+++ b/src/Init/Lean/Meta/Tactic/Assert.lean
@@ -19,7 +19,7 @@ withMVarContext mvarId $ do
   target ← getMVarType mvarId;
   let newType := Lean.mkForall name BinderInfo.default type target;
   newMVar ← mkFreshExprSyntheticOpaqueMVar newType tag;
-  modify $ fun s => { mctx := s.mctx.assignExpr mvarId (mkApp newMVar val), .. s };
+  assignExprMVar mvarId (mkApp newMVar val);
   pure newMVar.mvarId!
 
 /--
@@ -32,7 +32,7 @@ withMVarContext mvarId $ do
   target ← getMVarType mvarId;
   let newType := Lean.mkLet name type val target;
   newMVar ← mkFreshExprSyntheticOpaqueMVar newType tag;
-  modify $ fun s => { mctx := s.mctx.assignExpr mvarId newMVar, .. s };
+  assignExprMVar mvarId newMVar;
   pure newMVar.mvarId!
 
 end Meta
diff --git a/src/Init/Lean/Meta/Tactic/Clear.lean b/src/Init/Lean/Meta/Tactic/Clear.lean
index 330caf0a6b..4a017ab05d 100644
--- a/src/Init/Lean/Meta/Tactic/Clear.lean
+++ b/src/Init/Lean/Meta/Tactic/Clear.lean
@@ -30,7 +30,7 @@ withMVarContext mvarId $ do
     | none => localInsts
     | some idx => localInsts.eraseIdx idx;
   newMVar ← mkFreshExprMVarAt lctx localInsts mvarDecl.type tag MetavarKind.syntheticOpaque;
-  modify $ fun s => { mctx := s.mctx.assignExpr mvarId newMVar, .. s };
+  assignExprMVar mvarId newMVar;
   pure newMVar.mvarId!
 
 end Meta
diff --git a/src/Init/Lean/Meta/Tactic/Intro.lean b/src/Init/Lean/Meta/Tactic/Intro.lean
index 5218f20c75..723b82e9f3 100644
--- a/src/Init/Lean/Meta/Tactic/Intro.lean
+++ b/src/Init/Lean/Meta/Tactic/Intro.lean
@@ -20,7 +20,7 @@ def introNCoreAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name → σ
       newMVar ← mkFreshExprSyntheticOpaqueMVar type tag;
       lctx    ← getLCtx;
       newVal  ← mkLambda fvars newMVar;
-      modify $ fun s => { mctx := s.mctx.assignExpr mvarId newVal, .. s };
+      assignExprMVar mvarId newVal;
       pure $ (fvars, newMVar.mvarId!)
 | (i+1), lctx, fvars, j, s, Expr.letE n type val body _ => do
   let type   := type.instantiateRevRange j fvars.size fvars;
diff --git a/src/Init/Lean/Meta/Tactic/Subst.lean b/src/Init/Lean/Meta/Tactic/Subst.lean
index b28a3710e4..bd3cc3090f 100644
--- a/src/Init/Lean/Meta/Tactic/Subst.lean
+++ b/src/Init/Lean/Meta/Tactic/Subst.lean
@@ -52,7 +52,7 @@ withMVarContext mvarId $ do
             newMVar ← mkFreshExprSyntheticOpaqueMVar newType tag;
             let minor := newMVar;
             newVal  ← if depElim then mkEqRec motive minor major else mkEqNDRec motive minor major;
-            modify $ fun s => { mctx := s.mctx.assignExpr mvarId newVal, .. s };
+            assignExprMVar mvarId newVal;
             let mvarId := newMVar.mvarId!;
             mvarId ← clear mvarId hFVarId;
             mvarId ← clear mvarId aFVarId;
diff --git a/src/Init/Lean/Meta/Tactic/Target.lean b/src/Init/Lean/Meta/Tactic/Target.lean
index 088b0a9e3c..a493655c3b 100644
--- a/src/Init/Lean/Meta/Tactic/Target.lean
+++ b/src/Init/Lean/Meta/Tactic/Target.lean
@@ -23,7 +23,7 @@ withMVarContext mvarId $ do
   eq      ← mkEq target newTarget;
   let newProof := mkApp2 (mkConst `id [levelZero]) eq eqProof; -- checkpoint for eqProof
   let newVal := mkAppN (Lean.mkConst `Eq.mpr [u]) #[target, newTarget, eqProof, newMVar];
-  modify $ fun s => { mctx := s.mctx.assignExpr mvarId newMVar, .. s };
+  assignExprMVar mvarId newMVar;
   pure newMVar.mvarId!
 
 /--
@@ -43,7 +43,7 @@ withMVarContext mvarId $ do
     newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag;
     u       ← getLevel target;
     let newVal := mkApp2 (Lean.mkConst `id [u]) target newMVar;
-    modify $ fun s => { mctx := s.mctx.assignExpr mvarId newMVar, .. s };
+    assignExprMVar mvarId newMVar;
     pure newMVar.mvarId!
 
 end Meta