fix: use getTransparency in librarySearch SolveByElim.Config (#566)

Std/Tactic/LibrarySearch.lean

@@ -366,7 +366,8 @@ def solveByElim (required : List Expr) (exfalso : Bool) (goals : List MVarId) (m
   -- There is only a marginal decrease in performance for using the `symm` option for `solveByElim`.
   -- (measured via `lake build && time lake env lean test/librarySearch.lean`).
   let cfg : SolveByElim.Config :=
-    { maxDepth, exfalso := exfalso, symm := true, commitIndependentGoals := true }
+    { maxDepth, exfalso := exfalso, symm := true, commitIndependentGoals := true,
+      transparency := ← getTransparency }
   let ⟨lemmas, ctx⟩ ← SolveByElim.mkAssumptionSet false false [] [] #[]
   let cfg := if !required.isEmpty then cfg.requireUsingAll required else cfg
   SolveByElim.solveByElim cfg lemmas ctx goals

test/library_search/basic.lean

@@ -231,3 +231,10 @@ warning: declaration uses 'sorry'
 #guard_msgs in
 example {x : Int} (h : x ≠ 0) : 2 * x ≠ 0 := by
   std_apply? using h
+
+-- Check that adding `with_reducible` prevents expensive kernel reductions.
+-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60exact.3F.60.20failure.3A.20.22maximum.20recursion.20depth.20has.20been.20reached.22/near/417649319
+/-- info: Try this: exact Nat.add_comm n m -/
+#guard_msgs in
+example (_h : List.range 10000 = List.range 10000) (n m : Nat) : n + m = m + n := by
+  with_reducible std_exact?