chore(cmd/where): remove unused argument (#2486)
chore(cmd/where): remove unused argument (#2486)

Just remove an unused argument from the `#where` declaration, satisfying the linter.

<br>
<br>
<br>





leanprover-community/mathlib,leanprover-community/mathlib