feat(library/tactic): expose more builtin tactics, cleanup expr_to_tactic procedure

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): improve error messages when users forget to import 'tactic'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/unifier): when projecting give preference to most recent locals

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(tests/lean/run): add 'apply subst' test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): add apply tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard): add congr theorem

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/unifier): missing case

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/unifier): reduce the number unify procedure 'flavors'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 feat(library/unifier): add 'quick' failure

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/lazy_list_fn): handle the 'is_nil' case more efficiently

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/unifier): eagerly apply substitution to improve quick failure

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): add eassumption tactic, and remove redundant 'subgoals' from apply tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>