.

src/Lean/Meta/Tactic/Clear.lean

@@ -43,9 +43,31 @@ def _root_.Lean.MVarId.tryClear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVar
   mvarId.clear fvarId <|> pure mvarId
 
 /--
-Try to erase the given free variables from the goal `mvarId`.
+Try to clear the given fvars from the local context.
+
+The fvars must be given in the order they appear in the local context.
+
+See also `tryClearMany'` which takes care of reordering internally,
+and returns the cleared hypotheses along with the new goal.
 -/
 def _root_.Lean.MVarId.tryClearMany (mvarId : MVarId) (fvarIds : Array FVarId) : MetaM MVarId := do
   fvarIds.foldrM (init := mvarId) fun fvarId mvarId => mvarId.tryClear fvarId
 
+/--
+Try to clear the given fvars from the local context. Returns the new goal and
+the hypotheses that were cleared.
+
+Does not require the `hyps` to be given in the order in which they
+appear in the local context.
+-/
+def _root_.Lean.MVarId.tryClearMany' (goal : MVarId) (fvarIds : Array FVarId) :
+    MetaM (MVarId × Array FVarId) :=
+  goal.withContext do
+    let fvarIds := (← getLCtx).sortFVarsByContextOrder fvarIds
+    fvarIds.foldrM (init := (goal, Array.mkEmpty fvarIds.size))
+      fun h (goal, cleared) => do
+        let goal' ← goal.tryClear h
+        let cleared := if goal == goal' then cleared else cleared.push h
+        return (goal', cleared)
+
 end Lean.Meta