fix: use default reducibility when proving equation theorems for definition

Addresses issue reported by @fpfu at #945

src/Lean/Meta/Match/MatchEqs.lean

@@ -187,7 +187,7 @@ partial def proveCondEqThm (matchDeclName : Name) (type : Expr) : MetaM Expr :=
     let mvar0  ← mkFreshExprSyntheticOpaqueMVar target
     let mvarId ← deltaTarget mvar0.mvarId! (. == matchDeclName)
     trace[Meta.Match.matchEqs] "{MessageData.ofGoal mvarId}"
-    go mvarId 0
+    withDefault <| go mvarId 0
     mkLambdaFVars ys (← instantiateMVars mvar0)
 where
   go (mvarId : MVarId) (depth : Nat) : MetaM Unit := withIncRecDepth do

tests/lean/run/eqTheoremForVec.lean

@@ -0,0 +1,9 @@
+inductive Vector (α : Type u): Nat → Type u where
+| nil : Vector α 0
+| cons (head : α) (tail : Vector α n) : Vector α (n+1)
+
+theorem Nat.lt_of_add_lt_add_right {a b c : Nat} (h : a + b < c + b) : a < c := sorry
+
+def Vector.nth : ∀{n}, Vector α n → Fin n → α
+| n+1, Vector.cons x xs, ⟨  0, _⟩ => x
+| n+1, Vector.cons x xs, ⟨k+1, h⟩ => xs.nth ⟨k, Nat.lt_of_add_lt_add_right h⟩