bug in unusedSimpArgs linter with simprocs

Stream: mathlib4

[Alex Meiburg]

In the following snippet:

import Mathlib

theorem extracted (α β : ℝ) (h_ne_ab : ¬β = α) :
    ( α * β * ( β - α ) ⁻¹ : ℝ ) = α * α * ( β - α ) ⁻¹ + α := by
  simp [ -one_div, field, sub_ne_zero.2 h_ne_ab ]

you get an unusedSimpArgs warning on the sub_ne_zero.2 h_ne_ab argument. But, this argument is used, by the field simproc. I guess that, since simp itself didn't use it, it doesn't get picked up. But the alternative would be something like

theorem extracted (α β : ℝ) (h_ne_ab : ¬β = α) :
    ( α * β * ( β - α ) ⁻¹ : ℝ ) = α * α * ( β - α ) ⁻¹ + α := by
  have := sub_ne_zero.2 h_ne_ab
  simp [ -one_div, field,  this]

which isn't too bad, but if it was simp only near the top of a proof, then you probably want to clear it, etc. etc. ... it's kind of messy. I'm not sure if this is a bug in the linter, in simp, or in the simproc, or just simply a path that was never considered in the design of the linter? I can't tell.

Tagging @Heather Macbeth in case you know something more about the field simproc that could be useful here

[Bhavik Mehta]

See #29041