From 519ccf5d9daf15f96faba3a52c2558468bf4700d Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Tue, 2 Dec 2025 13:11:32 +1100
Subject: [PATCH] feat: add `solve_by_elim +suggestions` (#11468)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds `+suggestions` support to `solve_by_elim`, following the
pattern established by `grind +suggestions` and `simp_all +suggestions`.

Gracefully handles invalid/nonexistent suggestions by filtering them out

🤖 Prepared with Claude Code

Co-authored-by: Claude <noreply@anthropic.com>
---
 src/Lean/Elab/Tactic/SolveByElim.lean         | 16 ++++
 src/Lean/Meta/Tactic/SolveByElim.lean         |  6 ++
 tests/lean/run/solve_by_elim_suggestions.lean | 76 +++++++++++++++++++
 3 files changed, 98 insertions(+)
 create mode 100644 tests/lean/run/solve_by_elim_suggestions.lean

diff --git a/src/Lean/Elab/Tactic/SolveByElim.lean b/src/Lean/Elab/Tactic/SolveByElim.lean
index 2a033f6528..4d574f1deb 100644
--- a/src/Lean/Elab/Tactic/SolveByElim.lean
+++ b/src/Lean/Elab/Tactic/SolveByElim.lean
@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Meta.Tactic.SolveByElim
 public import Lean.Elab.Tactic.Config
+public import Lean.LibrarySuggestions.Basic
 
 public section
 
@@ -108,6 +109,21 @@ def evalSolveByElim : Tactic
     else
       pure [← getMainGoal]
     let cfg ← elabConfig cfg
+    -- Add library suggestions if +suggestions is enabled
+    let add ← if cfg.suggestions then
+      let mainGoal ← getMainGoal
+      let suggestions ← LibrarySuggestions.select mainGoal { caller := some "solve_by_elim" }
+      let suggestionTerms ← suggestions.toList.filterMapM fun s => do
+        -- Only include suggestions for constants that exist
+        let env ← getEnv
+        if env.contains s.name then
+          let ident := mkCIdentFrom (← getRef) s.name (canonical := true)
+          return some (⟨ident⟩ : Term)
+        else
+          return none
+      pure (add ++ suggestionTerms)
+    else
+      pure add
     let [] ← processSyntax cfg o.isSome star add remove use goals |
       throwError "Internal error: `solve_by_elim` unexpectedly returned subgoals"
     pure ()
diff --git a/src/Lean/Meta/Tactic/SolveByElim.lean b/src/Lean/Meta/Tactic/SolveByElim.lean
index 1fab5b4782..62634568f5 100644
--- a/src/Lean/Meta/Tactic/SolveByElim.lean
+++ b/src/Lean/Meta/Tactic/SolveByElim.lean
@@ -100,6 +100,12 @@ structure SolveByElimConfig extends ApplyRulesConfig where
   intro : Bool := true
   /-- Try calling `constructor` if no lemmas apply. -/
   constructor : Bool := true
+  /--
+  If `suggestions` is `true`, `solve_by_elim` will invoke the currently configured library
+  suggestion engine on the current goal, and attempt to use the resulting suggestions as
+  additional lemmas.
+  -/
+  suggestions : Bool := false
 
 namespace SolveByElimConfig
 
diff --git a/tests/lean/run/solve_by_elim_suggestions.lean b/tests/lean/run/solve_by_elim_suggestions.lean
new file mode 100644
index 0000000000..c08af1d63e
--- /dev/null
+++ b/tests/lean/run/solve_by_elim_suggestions.lean
@@ -0,0 +1,76 @@
+import Lean.LibrarySuggestions.Basic
+import Lean.Elab.Tactic.SolveByElim
+
+-- First test without any library suggestions set up
+/--
+error: No library suggestions engine registered. (Add `import Lean.LibrarySuggestions.Default` to use Lean's built-in engine, or use `set_library_suggestions` to configure a custom one.)
+-/
+#guard_msgs in
+example : True := by
+  solve_by_elim +suggestions
+
+-- Set up an empty library suggestion engine
+set_library_suggestions (fun _ _ => pure #[])
+
+#guard_msgs in
+example : True := by
+  solve_by_elim +suggestions
+
+-- A custom proposition that solve_by_elim doesn't know about by default
+-- We use a custom non-defeq type so that `trivial` and `rfl` don't solve it
+inductive MyProp : Nat → Prop where
+  | intro37 : MyProp 37
+  | intro42 : MyProp 42
+
+theorem myPropThm37 : MyProp 37 := MyProp.intro37
+
+-- Without +suggestions (or explicit lemma), solve_by_elim should fail
+-- Note: need -constructor to prevent constructor from solving it
+/--
+error: failed
+-/
+#guard_msgs in
+example : MyProp 37 := by
+  solve_by_elim -constructor
+
+-- With explicit lemma, it works
+example : MyProp 37 := by
+  solve_by_elim only [myPropThm37]
+
+-- Set up library suggestion engine that suggests our theorem
+set_library_suggestions (fun _ _ => pure #[{ name := `myPropThm37, score := 1.0 }])
+
+-- With +suggestions, it should work
+example : MyProp 37 := by
+  solve_by_elim -constructor +suggestions
+
+-- Test that suggestions work with local hypotheses
+example (h : MyProp 42) : MyProp 42 := by
+  solve_by_elim +suggestions
+
+-- Test with chain of applications
+inductive IsZero : Nat → Prop where
+  | intro : IsZero 0
+
+def fromZero (n : Nat) (h : n = 0) : IsZero n := by
+  subst h
+  exact IsZero.intro
+
+theorem isZero_zero : IsZero 0 := IsZero.intro
+
+set_library_suggestions (fun _ _ => pure #[
+  { name := `isZero_zero, score := 1.0 }
+])
+
+example : IsZero 0 := by
+  solve_by_elim +suggestions
+
+-- Test with bad suggestions - they should be ignored silently
+set_library_suggestions (fun _ _ => pure #[
+  { name := `isZero_zero, score := 1.0 },
+  { name := `nonexistent_theorem, score := 0.5 }
+])
+
+-- Bad suggestions should be filtered out, and the good one should work
+example : IsZero 0 := by
+  solve_by_elim +suggestions