feat(tactic/obviously): improve error reporting (#3412)
If `obviously` (used for auto_params) fails, it now prints a more useful message than "chain tactic made no progress"
If the goal presented to obviously contains `sorry`, it just uses `sorry` to discard it.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
