diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
index c63f1ebfff48..6738dddb6b25 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
@@ -37,12 +37,12 @@ where
       return ()
     else if (← tryContradiction mvarId) then
       return ()
+    else if let some mvarId ← whnfReducibleLHS? mvarId then
+      go mvarId
     else if let some mvarId ← simpMatch? mvarId then
       go mvarId
     else if let some mvarId ← simpIf? mvarId then
       go mvarId
-    else if let some mvarId ← whnfReducibleLHS? mvarId then
-      go mvarId
     else match (← simpTargetStar mvarId {} (simprocs := {})).1 with
       | TacticResultCNM.closed => return ()
       | TacticResultCNM.modified mvarId => go mvarId
diff --git a/tests/lean/run/simp_eqn_bug.lean b/tests/lean/run/simp_eqn_bug.lean
new file mode 100644
index 000000000000..22f62770eb12
--- /dev/null
+++ b/tests/lean/run/simp_eqn_bug.lean
@@ -0,0 +1,10 @@
+@[simp] def f (a : Nat) (xs : List Nat) : Nat :=
+  match a with
+  | 25 => 0
+  | _  => match xs with
+   | []    => a
+   | x::xs => x + f a xs
+
+example : f 25 xs = 0 := by apply f._eq_1
+example (h : a = 25 → False) : f a [] = a := by apply f._eq_2; assumption
+example (h : a = 25 → False) : f a (x::xs) = x + f a xs := by apply f._eq_3; assumption