From 4fe56d2a9db64696a65e58b0b67dbc366fdec22b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 2 Feb 2022 13:19:23 -0800
Subject: [PATCH] fix: allow `mkElimApp` to assign new goals when solving
 typing constraints

---
 src/Lean/Elab/Tactic/Induction.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 4269ed7f4c..b32fc5eaf4 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -116,7 +116,7 @@ partial def mkElimApp (elimName : Name) (elimInfo : ElimInfo) (targets : Array E
           throwError "insufficient number of targets for '{elimName}'"
         let target := ctx.targets[s.targetPos]
         let expectedType ← getArgExpectedType
-        let target ← Term.ensureHasType expectedType target
+        let target ← withConfig (fun cfg => { cfg with assignSyntheticOpaque := true }) do Term.ensureHasType expectedType target
         modify fun s => { s with targetPos := s.targetPos + 1 }
         addNewArg target
       else match c.binderInfo with
@@ -150,7 +150,8 @@ partial def mkElimApp (elimName : Name) (elimInfo : ElimInfo) (targets : Array E
     catch _ =>
       setMVarKind mvarId MetavarKind.syntheticOpaque
       others := others.push mvarId
-  return { elimApp := (← instantiateMVars s.f), alts := s.alts, others := others }
+  let alts ← s.alts.filterM fun alt => return !(← isExprMVarAssigned alt.2)
+  return { elimApp := (← instantiateMVars s.f), alts, others := others }
 
 /- Given a goal `... targets ... |- C[targets]` associated with `mvarId`, assign
   `motiveArg := fun targets => C[targets]` -/