From 94641e88cf4e62ef89e67823f28ec3b114b587e0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 15 Dec 2024 00:13:30 +0100
Subject: [PATCH] fix: `simp_all?` local declarations (#6385)

This PR fixes a bug in `simp_all?` that caused some local declarations
to be omitted from the `Try this:` suggestions.

closes #3519
---
 src/Lean/Elab/Tactic/SimpTrace.lean | 12 ++++++------
 tests/lean/run/3519.lean            | 13 ++++++++++++-
 2 files changed, 18 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Elab/Tactic/SimpTrace.lean b/src/Lean/Elab/Tactic/SimpTrace.lean
index 2bc4f649fc..7af839b06f 100644
--- a/src/Lean/Elab/Tactic/SimpTrace.lean
+++ b/src/Lean/Elab/Tactic/SimpTrace.lean
@@ -22,10 +22,10 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
   let stx := stx.unsetTrailing
   mkSimpOnly stx usedSimps
 
-@[builtin_tactic simpTrace] def evalSimpTrace : Tactic := fun stx =>
+@[builtin_tactic simpTrace] def evalSimpTrace : Tactic := fun stx => withMainContext do withSimpDiagnostics do
   match stx with
   | `(tactic|
-      simp?%$tk $[!%$bang]? $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do withSimpDiagnostics do
+      simp?%$tk $[!%$bang]? $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) =>
     let stx ← if bang.isSome then
       `(tactic| simp!%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
     else
@@ -39,9 +39,9 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
     return stats.diag
   | _ => throwUnsupportedSyntax
 
-@[builtin_tactic simpAllTrace] def evalSimpAllTrace : Tactic := fun stx =>
+@[builtin_tactic simpAllTrace] def evalSimpAllTrace : Tactic := fun stx => withMainContext do withSimpDiagnostics do
   match stx with
-  | `(tactic| simp_all?%$tk $[!%$bang]? $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?) => withSimpDiagnostics do
+  | `(tactic| simp_all?%$tk $[!%$bang]? $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?) =>
     let stx ← if bang.isSome then
       `(tactic| simp_all!%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?)
     else
@@ -79,9 +79,9 @@ where
     | some mvarId => replaceMainGoal [mvarId]
     pure stats
 
-@[builtin_tactic dsimpTrace] def evalDSimpTrace : Tactic := fun stx =>
+@[builtin_tactic dsimpTrace] def evalDSimpTrace : Tactic := fun stx => withMainContext do withSimpDiagnostics do
   match stx with
-  | `(tactic| dsimp?%$tk $[!%$bang]? $cfg:optConfig $[only%$o]? $[[$args,*]]? $(loc)?) => withSimpDiagnostics do
+  | `(tactic| dsimp?%$tk $[!%$bang]? $cfg:optConfig $[only%$o]? $[[$args,*]]? $(loc)?) =>
     let stx ← if bang.isSome then
       `(tactic| dsimp!%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]? $(loc)?)
     else
diff --git a/tests/lean/run/3519.lean b/tests/lean/run/3519.lean
index 1647adf08b..2eabf3efac 100644
--- a/tests/lean/run/3519.lean
+++ b/tests/lean/run/3519.lean
@@ -6,5 +6,16 @@ warning: declaration uses 'sorry'
 #guard_msgs in
 example {P : Nat → Prop} : let x := 0; P x := by
   intro x
-  simp? [x] -- Try this: simp_all only
+  simp? [x]
+  sorry
+
+/--
+info: Try this: simp_all only [x]
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example {P : Nat → Prop} : let x := 0; P x := by
+  intro x
+  simp_all? [x]
   sorry