fix: substEqs may close input goal

closes #1029

src/Lean/Meta/Injective.lean

@@ -127,8 +127,8 @@ private def mkInjectiveEqTheoremValue (ctorName : Name) (targetType : Expr) : Me
     let (_, mvarId₂) ← intro1 mvarId₂
     solveEqOfCtorEq ctorName mvarId₁ h
     let mvarId₂ ← casesAnd mvarId₂
-    let mvarId₂ ← substEqs mvarId₂
-    applyRefl mvarId₂ (injTheoremFailureHeader ctorName)
+    if let some mvarId₂ ← substEqs mvarId₂ then
+      applyRefl mvarId₂ (injTheoremFailureHeader ctorName)
     mkLambdaFVars xs mvar
 
 private def mkInjectiveEqTheorem (ctorVal : ConstructorVal) : MetaM Unit := do

src/Lean/Meta/Tactic/Cases.lean

@@ -340,11 +340,11 @@ def casesAnd (mvarId : MVarId) : MetaM MVarId := do
   let mvarIds ← casesRec mvarId fun localDecl => return (← instantiateMVars localDecl.type).isAppOfArity ``And 2
   exactlyOne mvarIds
 
-def substEqs (mvarId : MVarId) : MetaM MVarId := do
+def substEqs (mvarId : MVarId) : MetaM (Option MVarId) := do
   let mvarIds ← casesRec mvarId fun localDecl => do
     let type ← instantiateMVars localDecl.type
     return type.isEq || type.isHEq
-  exactlyOne mvarIds
+  ensureAtMostOne mvarIds
 
 structure ByCasesSubgoal where
   mvarId : MVarId

tests/lean/run/1029.lean

@@ -0,0 +1,2 @@
+inductive Foo : Type
+  | mk : 0 = 1 → Foo → Foo