Commit 2023-04-21 02:11 ed7dde1e

chore: simplify how solve_by_elim works when not backtracking (#3480) 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 https://github.com/leanprover-community/mathlib4/pull/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 https://github.com/leanprover-community/mathlib4/pull/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.