New std4 linters

Stream: lean4

[Mario Carneiro]

I just want to advertise two cool new linters that were just added to Std:

• The "unreachable tactic" linter will warn if a tactic is never called, for example if you do something like simp <;> apply foobar you might not notice that foobar doesn't actually exist because simp closed the goal.
• The "unnecessary <;>" linter will warn if you use tac1 <;> tac2 when tac1 only produces one subgoal. This is amazing for lean 3 porting!

I'm open to upstreaming these to lean core if desired (these use the lean core linter framework).