diff --git a/src/Lean/Meta/Injective.lean b/src/Lean/Meta/Injective.lean
index 6b0a997dff..a0ba276eb9 100644
--- a/src/Lean/Meta/Injective.lean
+++ b/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
diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean
index 8afc43bb9c..968bac7522 100644
--- a/src/Lean/Meta/Tactic/Cases.lean
+++ b/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
diff --git a/tests/lean/run/1029.lean b/tests/lean/run/1029.lean
new file mode 100644
index 0000000000..0b3a6245a9
--- /dev/null
+++ b/tests/lean/run/1029.lean
@@ -0,0 +1,2 @@
+inductive Foo : Type
+  | mk : 0 = 1 → Foo → Foo