refactor: add findLocalDeclWithType?

src/Lean/Meta/Tactic/Assumption.lean

@@ -8,24 +8,25 @@ import Lean.Meta.Tactic.Util
 
 namespace Lean.Meta
 
-def assumptionAux (mvarId : MVarId) : MetaM Bool :=
+/-- Return a local declaration whose type is definitionally equal to `type`. -/
+def findLocalDeclWithType? (type : Expr) : MetaM (Option FVarId) := do
+  (← getLCtx).findDeclRevM? fun localDecl => do
+    if localDecl.isAuxDecl then
+      return none
+    else if (← isDefEq type localDecl.type) then
+      return some localDecl.fvarId
+    else
+      return none
+
+def assumptionCore (mvarId : MVarId) : MetaM Bool :=
   withMVarContext mvarId do
     checkNotAssigned mvarId `assumption
-    let mvarType ← getMVarType mvarId
-    let lctx ← getLCtx
-    let h? ← lctx.findDeclRevM? fun decl => do
-      if decl.isAuxDecl then
-        pure none
-      else if (← isDefEq mvarType decl.type) then
-        pure (some decl.toExpr)
-      else
-        pure none
-    match h? with
-    | some h => do assignExprMVar mvarId h; pure true
-    | none   => pure false
+    match (← findLocalDeclWithType? (← getMVarType mvarId)) with
+    | none => return false
+    | some fvarId => assignExprMVar mvarId (mkFVar fvarId); return true
 
 def assumption (mvarId : MVarId) : MetaM Unit :=
-  unless (← assumptionAux mvarId) do
+  unless (← assumptionCore mvarId) do
     throwTacticEx `assumption mvarId ""
 
 end Lean.Meta