feat: register mathlib tactics with try?

Stream: PR reviews

[Kim Morrison]

https://github.com/leanprover-community/mathlib4-nightly-testing/pull/136 registers some tactics currently registered with hint also with try?.

Note that try? has a different scope than hint: it is mostly only trying to close goals, not give suggestions of tactics that make progress. This explains some of the omissions from hint registrations. (Note that there is the try? +missing flag, which does attempt to build partial proofs with sorry, but there's no current mechanism for user extensions to register with this. Please let me know if this is desirable.)

I've also not registered linarith and ring, since try? tries grind first, and only attempts user extensions if that (and simp_all, and exact?, and a few others) has failed.

[Kim Morrison]

This is a PR to bump/v4.27.0 rather than master as it requires features that will land in v4.27.0-rc1. I think it can be reviewed/discussed/merged as normal in the meantime.

[Kim Morrison]

(Sorry, this had been broken, but is now fixed I think and ready for review/merge.)

[Johan Commelin]

LGTM