feat(tactic/lint): add linter for simp lemmas whose lhs has a variable as head symbol

[gebner]

Motivation: you write a very useful simp lemma ∀ f : ℕ → ℕ, ∀ x, f x = 0. But it doesn't work. What happened? The simplifier indexes each simp lemma by the head symbol of the left-hand side. In this case it is f---however it is a fresh temporary meta variable created when adding the simp lemma to the simp set. Since this meta variable does not occur anywhere else, the lemma will never fire.

This PR introduces a linter for such simp lemmas and fixes all issues in mathlib.

[robertylewis]

Nice! I'm happy there were only a few failing declarations here.

[robertylewis]

I think this is ready too, but #2041 will cause merge conflicts, so let's update this after that one lands.

[robertylewis]

Wait, does this still add the new linter to CI?

Edit -- yes, I think it does, all good.

[gebner]

Since #2041, the CI automatically uses all the default linters. There was one linter that we didn't run in CI, namely has_inhabited_instance, which I originally didn't enable by default because I didn't know how to update nolints.txt.

If we want to run fewer or more linters in CI than in the default set, the mathlib_linters definition should be modified here (by erasing/adding elements from/to the list):

mathlib/src/tactic/lint.lean

Line 675 in 0fc45dc

let ls := ls.map (λ ⟨n, _⟩, `linter ++ n),

[robertylewis]

I think we originally set it up to list the CI linters explicitly, in case someone wanted to add a new linter that we didn't want in CI. But this can be done just by not tagging it with @[linter].