`simp [...]` with a left arrow (`←`) on a simproc should error

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The syntax of simp [...] allows prefixing an identifier with ←, but this doesn't affect simprocs and is silently ignored.

Steps to Reproduce

example : True := by
  simp [← seval]

example : 3 ∣ 9 := by
  simp [← Nat.reduceDvd]

Expected behavior: Log an error message "← cannot be used on simprocs" or similar.

Actual behavior: No error messages are logged.

Versions

Lean 4.36.0-nightly-2026-09-16
Target: x86_64-unknown-linux-gnu Linux

Additional Information

I think this is the relevant code, where there's a boolean inv of whether a left arrow was specified, and then there's a match on the type of the argument, and inv is ignored in the case of simprocs.
It is also ignored for ext, so presumably simp sets have the same issue.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start in src/Lean/Elab/Tactic/Simp.lean around lines 358-370, where the inv flag is matched against the argument type. Reproduce the examples with simp [← seval] and simp [← Nat.reduceDvd]. Done means a clear error such as "← cannot be used on simprocs" is reported instead of silently ignoring the arrow.