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.

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