fix: backtrack at `injection` failure This PR fixes an issue in the `injection` tactic. This tactic may execute multiple sub-tactics. If any of them fail, we must backtrack the partial assignment. This issue was causing the error: "`mvarId` is already assigned" in issue #6066. The issue is not yet resolved, as the equation generator for the match expressions is failing in the example provided in this issue.
This is the repository for Lean 4.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean (documentation source: doc/make/index.md).