fix: unset trailing for simpa? "try this" suggestion (#5907)

Closes #4581
leanprover · Nov 8, 2024 · 85f2213 · 85f2213
1 parent 9b167e2
commit 85f2213
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/Lean/Elab/Tactic/Simpa.lean b/src/Lean/Elab/Tactic/Simpa.lean
@@ -95,7 +95,8 @@ deriving instance Repr for UseImplicitLambdaResult
       else
         g.assumption; pure stats
       if tactic.simp.trace.get (← getOptions) || squeeze.isSome then
-        let stx ← match ← mkSimpOnly stx stats.usedTheorems with
+        let usingArg : Option Term := usingArg.map (⟨·.raw.unsetTrailing⟩)
+        let stx ← match ← mkSimpOnly stx.raw.unsetTrailing stats.usedTheorems with
           | `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?) =>
             if unfold.isSome then
               `(tactic| simpa! $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)