fix: unfold x<y in discrimination tree module

src/Lean/Meta/DiscrTree.lean

@@ -259,7 +259,7 @@ where
   step (e : Expr) := do
     let e ← whnfCore e
     match (← unfoldDefinition? e) with
-    | some e' => if isBadKey e' then return e else step e'
+    | some e' => if isBadKey e'.getAppFn then return e else step e'
     | none    => return e
 
 /-- whnf for the discrimination tree module -/

tests/lean/run/simpUnfoldAbbrev.lean

@@ -0,0 +1,14 @@
+example {x y : Nat} (h : y > x) : x < y := by
+  -- simp should unfold `>` when inserting into the discrimination tree
+  simp [h]
+
+abbrev good (n : Nat) :=
+  n > 42
+
+example (h : good n) : n > 42 := by
+  -- simp should unfold `good` when inserting into the discrimination tree
+  simp [h]
+
+example {x y : Nat} (h : x ≠ y) : x ≠ y := by
+  -- ≠ is also an abbreviation
+  simp [h]