diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 3a27816504..7696948214 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -2005,6 +2005,18 @@ lbool type_context::is_def_eq_lazy_delta(expr & t, expr & s) {
                         s = whnf_core(*unfold_definition(s));
                     }
                 }
+                /* If we haven't reduced t nor s, and they do not contain metavariables,
+                   then we try to use the definitional height to decide which one we will unfold
+                   (i.e., we mimic the behavior of the kernel type checker. */
+                if (!progress && !has_expr_metavar(t) && !has_expr_metavar(s)) {
+                    if (!d_t->is_theorem() && d_t->get_height() > d_s->get_height()) {
+                        progress = true;
+                        t        = whnf_core(*unfold_definition(t));
+                    } else if (!d_s->is_theorem() && d_t->get_height() < d_s->get_height()) {
+                        progress = true;
+                        s        = whnf_core(*unfold_definition(s));
+                    }
+                }
                 /* If we haven't reduced t nor s, then we reduce both IF the reduction is productive.
                    That is, the result of the reduction is not a recursor application. */
                 if (!progress) {
diff --git a/tests/lean/run/is_def_eq_perf_bug.lean b/tests/lean/run/is_def_eq_perf_bug.lean
new file mode 100644
index 0000000000..013efee25a
--- /dev/null
+++ b/tests/lean/run/is_def_eq_perf_bug.lean
@@ -0,0 +1,7 @@
+definition f (n : nat) : nat :=
+if n = 100000 then 1 else 0
+
+open tactic
+
+example (n : nat) : f 100000 = (if (100000 : nat) = 100000 then 1 else 0) :=
+by reflexivity