Merging primed tactics

[digama0]

Mathlib has a bunch of primed tactics, which either fix bugs or do things slightly differently than the unprimed tactics. We should go through the list and merge as many as possible. (We will then introduce a bunch more primed tactics of our own, when needed to disambiguate with lean 4 tactics.)

Here is a list of primed tactics found so far:

• apply', fapply', eapply', apply_with', mapply', refl', symmetry', transitivity': These all seem to be dealing with the same bug in apply. I think they can be merged.
• guard_hyp', guard_expr_eq', guard_target': this does something different from the unprimed tactics, they use strict equality instead of alpha-equal. I've accomodated this with different syntax in the tactic.
• change': from the docstring it sounds like a bugfix. Merge?
• generalize': bugfix, merge
• subst': bugfix, merge
• clear': bugfix, merge
• congr': bugfix + generalized syntax, merge
• measurability': the unprimed tactic also exists in mathlib, this seems to be working around a limitation in lean 3 auto params, drop?