fix: bug in apply? when using intro

leanprover · Oct 2, 2024 · 160c0f1 · 160c0f1
1 parent 1329a26
commit 160c0f1
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/src/Lean/Elab/Tactic/LibrarySearch.lean b/src/Lean/Elab/Tactic/LibrarySearch.lean
@@ -23,7 +23,6 @@ Implementation of the `exact?` tactic.
 -/
 def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireClose : Bool) :
     TacticM Unit := do
-  let mvar ← getMainGoal
   let (_, goal) ← (← getMainGoal).intros
   goal.withContext do
     let required := (← (required.getD #[]).mapM getFVarId).toList.map .fvar
@@ -35,15 +34,15 @@ def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireCl
     match ← librarySearch goal tactic allowFailure with
     -- Found goal that closed problem
     | none =>
-      addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta
+      addExactSuggestion ref (← instantiateMVars (mkMVar goal)).headBeta
     -- Found suggestions
     | some suggestions =>
       if requireClose then throwError
         "`exact?` could not close the goal. Try `apply?` to see partial suggestions."
       reportOutOfHeartbeats `library_search ref
       for (_, suggestionMCtx) in suggestions do
         withMCtx suggestionMCtx do
-          addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta (addSubgoalsMsg := true)
+          addExactSuggestion ref (← instantiateMVars (mkMVar goal)).headBeta (addSubgoalsMsg := true)
       if suggestions.isEmpty then logError "apply? didn't find any relevant lemmas"
       admitGoal goal