Make `compose` a notation rather than a definition

This makes life a lot easier; we don't have to be constantly unfolding it, and we can avoid `Local Arguments compose /.` and `simpl rewrite` in lots of places.
Oh, darn, I meant to come back to this and then forgot.  Yes, the concat ones work, I shouldn't have commented those out.  I'm not sure why the compose ones break; do you have any guesses?  The error is `Found no subterm matching "fun x : A => ?M97 (f (g x))" in the current goal.`  It seems that these tactics might still be useful even with `compose` as a notation, so I'd like to keep them if possible.