chore: use binderIdent consistently in grammar

[digama0]

This PR normalizes usage of binderIdent vs ident across the lean grammar. To construct this PR I reviewed every occurrence of ident to determine whether (1) it is introducing a new binding and (2) it would make sense to be allowed to use _ with the meaning of introducing an unnamed (hygienic automatically named) variable, especially in cases where the unused variables linter might fire.

Currently the PR does not compile because there will be some staging and other bugfixing regarding the use and implementation of the _ part of these commands. Before proceeding I would like a thumbs-up regarding all (or a subset of) the grammar changes proposed here. In the examples below each occurrence of _x represents an ident that would be allowed to be _ under the proposal.

1. { _x // e }
2. by intros _x
3. by rename a => _x
4. by injection e with _x
5. by injections _x
6. by have' _x := e
7. by generalize _x : e = _x
8. by cases _x : e
9. termination_by' _x => e
10. decreasing_by _x => tac
11. initialize _x : e <- e
12. notation "foo" _x => e
13. macro "foo" _x:cat : cat => e
14. match _x : e with | _x@pat => e
15. let _x y := e; e
16. have _x y := e; e

Additionally, places which used ident <|> hole for binders were changed to use binderIdent. This decreases the amount of ad-hoc special casing required in programs consuming and constructing lean syntax like mathport. (Unfortunately there is still some conversion required to go from binderIdent to term, since the _ case is represented differently in each case.)