feat: admit alternatives that failed

src/Lean/Elab/Tactic/Basic.lean

@@ -226,6 +226,18 @@ def focusAux {α} (tactic : TacticM α) : TacticM α := do
 def focus {α} (tactic : TacticM α) : TacticM α :=
   focusAux do let a ← tactic; done; pure a
 
+/- Close the main goal using the given tactic. If it fails, log the error and `admit` -/
+def closeUsingOrAdmit (tac : Syntax) : TacticM Unit := do
+  let (mvarId, rest) ← getMainGoal
+  try
+    evalTactic tac
+    done
+  catch ex =>
+    logException ex
+    let mvarType ← inferType (mkMVar mvarId)
+    assignExprMVar mvarId (← mkSorry mvarType (synthetic := true))
+    setGoals rest
+
 def try? {α} (tactic : TacticM α) : TacticM (Option α) := do
   try pure (some (← tactic))
   catch _ => pure none

src/Lean/Elab/Tactic/Induction.lean

@@ -169,8 +169,7 @@ def evalAlts (elimInfo : ElimInfo) (alts : Array (Name × MVarId)) (altsSyntax :
         for fvarId in toClear do
           altMVarId ← tryClear altMVarId fvarId
         setGoals [altMVarId]
-        evalTactic altRhs
-        done
+        closeUsingOrAdmit altRhs
   if usedWildcard then
     altsSyntax := altsSyntax.filter fun alt => getAltName alt != `_
   unless altsSyntax.isEmpty do
@@ -409,8 +408,7 @@ private def processResult (altRHSs : Array Syntax) (result : Array Meta.Inductio
         gs := gs ++ gs'
       else
         setGoals [mvarId]
-        evalTactic rhs
-        done
+        closeUsingOrAdmit rhs
     setGoals gs
 
 private def generalizeTerm (term : Expr) : TacticM Expr := do