Commit 2022-11-20 09:34 23e5bef3

feat: bring solve_by_elim closer to parity with mathlib3 (#629)

• Adds trivial, rfl, congrFun, and congrArg lemmas by default.
• Defers elaboration, to support cases where a lemma's implicit parameters must be instantiated more than once.
• Improves backtracking by working in the TacticM monad. In the old MetaM version, the recursive call only represents the work on a single subgoal, which may succeed but then later lead us to a dead end. With TacticM as done in the PR, it's natural for the recursive call to represent the entire remaining proof, including non-main subgoals.
• Adds tests to exercise all of these new features. Compare to the mathlib3 version.