diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 8217142ae4..3cd0c84e29 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -3600,7 +3600,7 @@ expr elaborator::get_default_numeral_type() {
 void elaborator::synthesize_numeral_types() {
     for (expr const & A : m_numeral_types) {
         if (is_metavar(instantiate_mvars(A))) {
-            if (!assign_mvar(A, get_default_numeral_type()))
+            if (!is_def_eq(A, get_default_numeral_type()))
                 report_or_throw(elaborator_exception(A, "invalid numeral, failed to force numeral to be a nat"));
         }
     }
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 685a42fdd5..5ed67daaf0 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -116,7 +116,6 @@ private:
     expr try_to_pi(expr const & e) { return m_ctx.try_to_pi(e); }
     bool is_def_eq(expr const & e1, expr const & e2);
     bool try_is_def_eq(expr const & e1, expr const & e2);
-    bool assign_mvar(expr const & e1, expr const & e2) { lean_assert(is_metavar(e1)); return is_def_eq(e1, e2); }
     bool is_uvar_assigned(level const & l) const { return m_ctx.is_assigned(l); }
     bool is_mvar_assigned(expr const & e) const { return m_ctx.is_assigned(e); }