From a11bdfc39e95fa5b09e06638a43bd8bd2eddce12 Mon Sep 17 00:00:00 2001
From: David Renshaw <dwrenshaw@gmail.com>
Date: Mon, 29 Jan 2024 20:46:52 -0500
Subject: [PATCH] fix: use getTransparency in librarySearch SolveByElim.Config
 (#566)

---
 Std/Tactic/LibrarySearch.lean  | 3 ++-
 test/library_search/basic.lean | 7 +++++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/Std/Tactic/LibrarySearch.lean b/Std/Tactic/LibrarySearch.lean
index f19de28a11..209a5416a8 100644
--- a/Std/Tactic/LibrarySearch.lean
+++ b/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
diff --git a/test/library_search/basic.lean b/test/library_search/basic.lean
index 91ff145210..9d1e33dc7f 100644
--- a/test/library_search/basic.lean
+++ b/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?