diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index 2298f89163..230c925618 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -154,7 +154,7 @@ where
       go mvarId
     else if let some mvarId ← simpMatch? mvarId then
       go mvarId
-    else if let some mvarIds ← splitTarget? mvarId then
+    else if let some mvarIds ← splitTarget? mvarId (splitIte := false) then
       mvarIds.forM go
     else
       saveEqn mvarId
@@ -239,7 +239,7 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
       go mvarId
     else if let some mvarId ← simpMatch? mvarId then
       go mvarId
-    else if let some mvarIds ← splitTarget? mvarId then
+    else if let some mvarIds ← splitTarget? mvarId (splitIte := false) then
       mvarIds.forM go
     else
      throwError "failed to generate unfold theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
diff --git a/tests/lean/run/heapSort.lean b/tests/lean/run/heapSort.lean
index 1b8f2db02a..34a8b68ffe 100644
--- a/tests/lean/run/heapSort.lean
+++ b/tests/lean/run/heapSort.lean
@@ -174,3 +174,5 @@ decreasing_by assumption
 
 attribute [simp] Array.heapSort.loop
 #check @Array.heapSort.loop._eq_1
+
+attribute [simp] BinaryHeap.heapifyDown
diff --git a/tests/lean/run/structuralEqns2.lean b/tests/lean/run/structuralEqns2.lean
index bb96df04cf..4d9d9a1fac 100644
--- a/tests/lean/run/structuralEqns2.lean
+++ b/tests/lean/run/structuralEqns2.lean
@@ -14,7 +14,6 @@ def g (i j : Nat) : Nat :=
 #eval tst ``g
 #check g._eq_1
 #check g._eq_2
-#check g._eq_3
 #check g._unfold
 
 def h (i j : Nat) : Nat :=
diff --git a/tests/lean/run/wfEqns2.lean b/tests/lean/run/wfEqns2.lean
index e9c08f9e8c..af26806193 100644
--- a/tests/lean/run/wfEqns2.lean
+++ b/tests/lean/run/wfEqns2.lean
@@ -33,7 +33,6 @@ decreasing_by
 #eval tst ``g
 #check g._eq_1
 #check g._eq_2
-#check g._eq_3
 #check g._unfold
 #eval tst ``h
 #check h._eq_1