Linter for unused variable declarations

[madvorak]

In the same way we have a linter for to detect an unused argument of a function or lemma, we should have a linter to detect an unused variable declaration. I realized we have many of them.

[b-mehta]

cc @adomani who has a version of this and has applied it in mathlib a few times.

[adomani]

I agree! There is a linter at #17715, but there are thousands of unused variables and I am still honing the logic behind the linter.

Once I fixed the currently known false positives, I'll probably ask for help removing the exceptions.