feat(tactic/tauto): optional closer tactic for `tauto` (#4189)
`tauto` sometimes fails on easy subgoals; instead of backtracking
and discarding the work, the user can now supply a closer tactic
to the remaining goals, such as `cc`, `simp`, or `linarith`.
this also wraps `tauto` in a `focus1`, which allows for better
error messages.
Co-authored-by: Jesse Michael Han <39395247+jesse-michael-han@users.noreply.github.com>
