This is a thorough refactor of `solve_by_elim`.

* Bug fixes and additional tests.
* Support for removing local hypotheses using `solve_by_elim [-h]`.
* Use `symm` on hypotheses and `exfalso` on the goal, as needed.
* To support that, `MetaM` level tooling for the `symm` tactic. (`rfl` and `trans` deserve the same treatment at some point.)
* Additional hooks for flow control in `solve_by_elim` (suspending goals to return to the user, rejecting branches, running arbitrary procedures on the goals).
* Using those hooks, reimplement `apply_assumption` and `apply_rules` as thin wrappers around `solve_by_elim`, allowing access to new features (removing hypotheses, symm and exfalso) for free.
* Using those hooks, fix `library_search using` so 
```example (P Q : List ℕ) (h : ℕ) : List ℕ := by library_search using P, Q -- exact P ∩ Q```

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

This is a thorough refactor of `solve_by_elim`.

* Bug fixes and additional tests.
* Support for removing local hypotheses using `solve_by_elim [-h]`.
* Use `symm` on hypotheses and `exfalso` on the goal, as needed.
* To support that, `MetaM` level tooling for the `symm` tactic. (`rfl` and `trans` deserve the same treatment at some point.)
* Additional hooks for flow control in `solve_by_elim` (suspending goals to return to the user, rejecting branches, running arbitrary procedures on the goals).
* Using those hooks, reimplement `apply_assumption` and `apply_rules` as thin wrappers around `solve_by_elim`, allowing access to new features (removing hypotheses, symm and exfalso) for free.
* Using those hooks, fix `library_search using` so 
```example (P Q : List ℕ) (h : ℕ) : List ℕ := by library_search using P, Q -- exact P ∩ Q```

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

…2302)

Fixes a bug introduced in #856.
If `solveByElim` succeeds, then we should return early. Otherwise, we look through all lemmas in the environment and find something like `namedPattern` or `Eq.mp` and unnecessarily wrap the result in that.

See #2276 for an example bad output caused by this bug.

Another example is this test: https://github.com/leanprover-community/mathlib4/blob/4ed65899eca4909e9b8f23a113b52ff8cb3f5d41/test/librarySearch.lean#L15
On master, it emits `exact namedPattern p p rfl`, and after this PR it correctly emits `exact p`.

…2302)

Fixes a bug introduced in #856.
If `solveByElim` succeeds, then we should return early. Otherwise, we look through all lemmas in the environment and find something like `namedPattern` or `Eq.mp` and unnecessarily wrap the result in that.

See #2276 for an example bad output caused by this bug.

Another example is this test: https://github.com/leanprover-community/mathlib4/blob/4ed65899eca4909e9b8f23a113b52ff8cb3f5d41/test/librarySearch.lean#L15
On master, it emits `exact namedPattern p p rfl`, and after this PR it correctly emits `exact p`.

We had some unfortunate spaghetti code in `solve_by_elim`. When @hrmacbeth had requested additional features for `apply_rules`, the easiest way to provide them was to re-use `solve_by_elim`'s parsing and lemma handling. (See #856.) However `apply_rules` doesn't to backtracking, and `solve_by_elim` is all about it. At the time, `solve_by_elim` didn't have clean separation between its "lemma application" and "backtracking" considerations, so the solution was to add some hacks the prevented the backtracking from actually occurring, in the backtracking code...

Since #2920, those considerations have been cleanly separated out. Thus it's possible to greatly simplify how we don't backtrack when we don't want to (in `apply_rules`). This PR does that.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

We had some unfortunate spaghetti code in `solve_by_elim`. When @hrmacbeth had requested additional features for `apply_rules`, the easiest way to provide them was to re-use `solve_by_elim`'s parsing and lemma handling. (See #856.) However `apply_rules` doesn't to backtracking, and `solve_by_elim` is all about it. At the time, `solve_by_elim` didn't have clean separation between its "lemma application" and "backtracking" considerations, so the solution was to add some hacks the prevented the backtracking from actually occurring, in the backtracking code...

Since #2920, those considerations have been cleanly separated out. Thus it's possible to greatly simplify how we don't backtrack when we don't want to (in `apply_rules`). This PR does that.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

We had some unfortunate spaghetti code in `solve_by_elim`. When @hrmacbeth had requested additional features for `apply_rules`, the easiest way to provide them was to re-use `solve_by_elim`'s parsing and lemma handling. (See #856.) However `apply_rules` doesn't to backtracking, and `solve_by_elim` is all about it. At the time, `solve_by_elim` didn't have clean separation between its "lemma application" and "backtracking" considerations, so the solution was to add some hacks the prevented the backtracking from actually occurring, in the backtracking code...

Since #2920, those considerations have been cleanly separated out. Thus it's possible to greatly simplify how we don't backtrack when we don't want to (in `apply_rules`). This PR does that.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

We had some unfortunate spaghetti code in `solve_by_elim`. When @hrmacbeth had requested additional features for `apply_rules`, the easiest way to provide them was to re-use `solve_by_elim`'s parsing and lemma handling. (See #856.) However `apply_rules` doesn't to backtracking, and `solve_by_elim` is all about it. At the time, `solve_by_elim` didn't have clean separation between its "lemma application" and "backtracking" considerations, so the solution was to add some hacks the prevented the backtracking from actually occurring, in the backtracking code...

Since #2920, those considerations have been cleanly separated out. Thus it's possible to greatly simplify how we don't backtrack when we don't want to (in `apply_rules`). This PR does that.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

We had some unfortunate spaghetti code in `solve_by_elim`. When @hrmacbeth had requested additional features for `apply_rules`, the easiest way to provide them was to re-use `solve_by_elim`'s parsing and lemma handling. (See #856.) However `apply_rules` doesn't to backtracking, and `solve_by_elim` is all about it. At the time, `solve_by_elim` didn't have clean separation between its "lemma application" and "backtracking" considerations, so the solution was to add some hacks the prevented the backtracking from actually occurring, in the backtracking code...

Since #2920, those considerations have been cleanly separated out. Thus it's possible to greatly simplify how we don't backtrack when we don't want to (in `apply_rules`). This PR does that.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>