From 7537fa779503bc05be94f5723ac1c320abeebfa9 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 23 Nov 2021 15:31:46 +0100
Subject: [PATCH] fix: unfold `x<y` in discrimination tree module

---
 src/Lean/Meta/DiscrTree.lean         |  2 +-
 tests/lean/run/simpUnfoldAbbrev.lean | 14 ++++++++++++++
 2 files changed, 15 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/simpUnfoldAbbrev.lean

diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index be65fe1d62..016d51da55 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/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 -/
diff --git a/tests/lean/run/simpUnfoldAbbrev.lean b/tests/lean/run/simpUnfoldAbbrev.lean
new file mode 100644
index 0000000000..8379ac3f77
--- /dev/null
+++ b/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]