fix: backtrack at injection failure (#6109)

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.

src/Lean/Meta/Tactic/Injection.lean

@@ -114,10 +114,11 @@ where
         if lhs.isRawNatLit && rhs.isRawNatLit then cont
         else
           try
-            match (← injection mvarId fvarId newNames) with
-            | .solved  => return .solved
-            | .subgoal mvarId newEqs remainingNames =>
-              mvarId.withContext <| go d (newEqs.toList ++ fvarIds) mvarId remainingNames
+            commitIfNoEx do
+              match (← injection mvarId fvarId newNames) with
+              | .solved  => return .solved
+              | .subgoal mvarId newEqs remainingNames =>
+                mvarId.withContext <| go d (newEqs.toList ++ fvarIds) mvarId remainingNames
           catch _ => cont
       else cont