feat: Meta.withErasedFVars (#4731)

this idiom shows up multiple times, is non-trivial (in the sense that
the `localInsts` has to be updated, and I am about to use it once more.
Hence time to abstract this out.

src/Lean/Elab/BuiltinTerm.lean

@@ -316,9 +316,7 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
           return false
     return true
   if canClear then
-    let lctx := (← getLCtx).erase fvarId
-    let localInsts := (← getLocalInstances).filter (·.fvar.fvarId! != fvarId)
-    withLCtx lctx localInsts do elabTerm body expectedType?
+    withErasedFVars #[fvarId] do elabTerm body expectedType?
   else
     elabTerm body expectedType?
 

src/Lean/Elab/Match.lean

@@ -672,8 +672,7 @@ partial def main (patternVarDecls : Array PatternVarDecl) (ps : Array Expr) (mat
         throwError "invalid patterns, `{mkFVar explicit}` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching{indentD (MessageData.joinSep (ps.toList.map (MessageData.ofExpr .)) m!"\n\n")}"
   let packed ← pack patternVars ps matchType
   trace[Elab.match] "packed: {packed}"
-  let lctx := explicitPatternVars.foldl (init := (← getLCtx)) fun lctx d => lctx.erase d
-  withTheReader Meta.Context (fun ctx => { ctx with lctx := lctx }) do
+  withErasedFVars explicitPatternVars do
     check packed
     unpack packed fun patternVars patterns matchType => do
       let localDecls ← patternVars.mapM fun x => x.fvarId!.getDecl

src/Lean/Meta/Basic.lean

@@ -1492,6 +1492,16 @@ private def withLocalContextImp (lctx : LocalContext) (localInsts : LocalInstanc
 def withLCtx (lctx : LocalContext) (localInsts : LocalInstances) : n α → n α :=
   mapMetaM <| withLocalContextImp lctx localInsts
 
+/--
+Runs `k` in a local envrionment with the `fvarIds` erased.
+-/
+def withErasedFVars [MonadLCtx n] [MonadLiftT MetaM n] (fvarIds : Array FVarId) (k : n α) : n α := do
+  let lctx ← getLCtx
+  let localInsts ← getLocalInstances
+  let lctx' := fvarIds.foldl (·.erase ·) lctx
+  let localInsts' := localInsts.filter (!fvarIds.contains ·.fvar.fvarId!)
+  withLCtx lctx' localInsts' k
+
 private def withMVarContextImp (mvarId : MVarId) (x : MetaM α) : MetaM α := do
   let mvarDecl ← mvarId.getDecl
   withLocalContextImp mvarDecl.lctx mvarDecl.localInstances x