From e76bbef79b18a7aa130a05d50cb9eca4e9ba2152 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Tue, 4 Nov 2025 16:26:51 +1100
Subject: [PATCH] feat: `simp? +suggestions` handles ambiguity (#11075)

This PR updates `simp? +suggestions` so that if a name is ambiguous
(because of namespaces) all alternatives are used, rather than erroring.
---
 src/Lean/Elab/Tactic/SimpTrace.lean  | 16 ++++++++++++----
 tests/lean/run/simp_suggestions.lean | 25 +++++++++++++++++++++++++
 2 files changed, 37 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/Tactic/SimpTrace.lean b/src/Lean/Elab/Tactic/SimpTrace.lean
index c35601a2cc..81e6bad87e 100644
--- a/src/Lean/Elab/Tactic/SimpTrace.lean
+++ b/src/Lean/Elab/Tactic/SimpTrace.lean
@@ -59,9 +59,13 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
       -- Get premise suggestions from the premise selector
       let suggestions ← Lean.LibrarySuggestions.select (← getMainGoal)
       -- Convert suggestions to simp argument syntax and add them to the args
+      -- If a name is ambiguous, we add ALL interpretations
       for sugg in suggestions do
-        let arg ← `(Parser.Tactic.simpLemma| $(mkIdent sugg.name):term)
-        argsArray := argsArray.push arg
+        let ident := mkIdent sugg.name
+        let candidates ← resolveGlobalConst ident
+        for candidate in candidates do
+          let arg ← `(Parser.Tactic.simpLemma| $(mkCIdentFrom ident candidate (canonical := true)):term)
+          argsArray := argsArray.push arg
     -- Build the simp syntax with the updated arguments
     let stxForExecution ← if bang.isSome then
       `(tactic| simp!%$tk $cfg:optConfig $[$discharger]? $[only%$o]? [$argsArray,*] $[$loc]?)
@@ -94,9 +98,13 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
       -- Get premise suggestions from the premise selector
       let suggestions ← Lean.LibrarySuggestions.select (← getMainGoal)
       -- Convert suggestions to simp argument syntax and add them to the args
+      -- If a name is ambiguous, we add ALL interpretations
       for sugg in suggestions do
-        let arg ← `(Parser.Tactic.simpLemma| $(mkIdent sugg.name):term)
-        argsArray := argsArray.push arg
+        let ident := mkIdent sugg.name
+        let candidates ← resolveGlobalConst ident
+        for candidate in candidates do
+          let arg ← `(Parser.Tactic.simpLemma| $(mkCIdentFrom ident candidate (canonical := true)):term)
+          argsArray := argsArray.push arg
     -- Build the simp_all syntax with the updated arguments
     let stxForExecution ←
       if argsArray.isEmpty then
diff --git a/tests/lean/run/simp_suggestions.lean b/tests/lean/run/simp_suggestions.lean
index 50462e14ee..98fc8b365a 100644
--- a/tests/lean/run/simp_suggestions.lean
+++ b/tests/lean/run/simp_suggestions.lean
@@ -59,3 +59,28 @@ error: +suggestions requires using simp_all? instead of simp_all
 example (a b : Nat) (h : myCustomAdd a b = myCustomAdd b a) : myCustomAdd a b = myCustomAdd b a := by
   simp_all +suggestions
   sorry
+
+-- Test ambiguous lemmas with DIFFERENT statements that are both needed
+-- Root version: left identity
+theorem myCustomAdd_id (x : Nat) : myCustomAdd 0 x = x := by
+  simp [myCustomAdd]
+
+-- Foo version: right identity
+theorem Foo.myCustomAdd_id (x : Nat) : myCustomAdd x 0 = x := by
+  simp [myCustomAdd]
+
+-- Set up premise selector that suggests the ambiguous name
+set_library_suggestions (fun _ _ => pure #[{ name := `myCustomAdd_id, score := 1.0 }])
+
+open Foo
+
+-- This goal needs BOTH lemmas to solve:
+-- myCustomAdd 0 a simplifies to a (using root version)
+-- myCustomAdd b 0 simplifies to b (using Foo version)
+/--
+info: Try this:
+  [apply] simp_all only [_root_.myCustomAdd_id, Foo.myCustomAdd_id]
+-/
+#guard_msgs in
+example (a b : Nat) (h : myCustomAdd 0 a = myCustomAdd b 0) : a = b := by
+  simp_all? +suggestions