From dda41cdc278e7b361a3d40c60e3c2502ed79ec10 Mon Sep 17 00:00:00 2001
From: David Renshaw <dwrenshaw@gmail.com>
Date: Sat, 27 Jan 2024 09:49:00 -0500
Subject: [PATCH] fix: use getTransparency in librarySearch SolveByElim.Config

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

diff --git a/Mathlib/Tactic/LibrarySearch.lean b/Mathlib/Tactic/LibrarySearch.lean
index 5855a99fd8aa4..05f1c2bd52bf4 100644
--- a/Mathlib/Tactic/LibrarySearch.lean
+++ b/Mathlib/Tactic/LibrarySearch.lean
@@ -104,7 +104,8 @@ def solveByElim (goals : List MVarId) (required : List Expr) (exfalso := false)
   -- 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 := depth, exfalso := exfalso, symm := true, commitIndependentGoals := true }
+    { maxDepth := depth, exfalso := exfalso, symm := true, commitIndependentGoals := true,
+      transparency := ← getTransparency }
   let cfg := if !required.isEmpty then cfg.requireUsingAll required else cfg
   SolveByElim.solveByElim.processSyntax cfg false false [] [] #[] goals
 
diff --git a/test/LibrarySearch/basic.lean b/test/LibrarySearch/basic.lean
index 5a101cdd77164..1fce4bfcbcbc8 100644
--- a/test/LibrarySearch/basic.lean
+++ b/test/LibrarySearch/basic.lean
@@ -236,3 +236,10 @@ example (P Q : Prop) (h : P → Q) (h' : ¬Q) : ¬P := by
 --   first
 --   | exact? says exact le_antisymm hxy hyx
 --   | exact? says exact ge_antisymm hyx hxy
+
+-- 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 exact?