chore: default for librarySearch tactic argument

src/Lean/Elab/Tactic/LibrarySearch.lean

@@ -67,8 +67,7 @@ def elabExact?Term : TermElab := fun stx expectedType? => do
     let goal ← mkFreshExprMVar expectedType
     let (_, introdGoal) ← goal.mvarId!.intros
     introdGoal.withContext do
-      let tactic := fun exfalso g => solveByElim []  (maxDepth := 6) exfalso g
-      if let some suggestions ← librarySearch introdGoal tactic then
+      if let some suggestions ← librarySearch introdGoal then
         reportOutOfHeartbeats `library_search stx
         for suggestion in suggestions do
           withMCtx suggestion.2 do

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -386,7 +386,8 @@ unless the goal was completely solved.)
 this is not currently tracked.)
 -/
 def librarySearch (goal : MVarId)
-    (tactic : Bool → List MVarId → MetaM (List MVarId))
+    (tactic : Bool → List MVarId → MetaM (List MVarId) :=
+      fun initial g => solveByElim [] (maxDepth := 6) (exfalso := initial) g)
     (allowFailure : MVarId → MetaM Bool := fun _ => pure true)
     (leavePercentHeartbeats : Nat := 10) :
     MetaM (Option (Array (List MVarId × MetavarContext))) := do