fix(tactic/lint): simp_nf: do not ignore errors (#2266)
This PR fixes some bugs in the `simp_nf` linter. Previously it ignored all errors (from failing tactics). I've changed this so that errors from linters are handled centrally and reported as linter warnings. The `simp_is_conditional` function was also broken.
As usual, new linters find new issues:
1. Apparently Lean sometimes throws away simp lemmas. https://github.com/leanprover-community/lean/issues/163
2. Some types define `has_coe` but have an incorrect `has_coe_to_fun`, causing the simplifier to loop `⇑f a = ⇑↑f a = ⇑f a`. See the new library note:
