diff --git a/src/library/tactic/defeq_simplifier/defeq_simplifier.cpp b/src/library/tactic/defeq_simplifier/defeq_simplifier.cpp
index 0b020314e1..882387ea63 100644
--- a/src/library/tactic/defeq_simplifier/defeq_simplifier.cpp
+++ b/src/library/tactic/defeq_simplifier/defeq_simplifier.cpp
@@ -350,6 +350,11 @@ vm_obj tactic_defeq_simp(vm_obj const & m, vm_obj const & e, vm_obj const & s0)
     LEAN_TACTIC_CATCH(s);
 }
 
+expr defeq_simplify(type_context & ctx, expr const & e) {
+    defeq_simp_lemmas lemmas  = get_defeq_simp_lemmas(ctx.env());
+    return defeq_simplify(ctx, lemmas, e);
+}
+
 /* Setup and teardown */
 void initialize_defeq_simplifier() {
     DECLARE_VM_BUILTIN(name({"tactic", "defeq_simp_core"}), tactic_defeq_simp);
diff --git a/src/library/tactic/defeq_simplifier/defeq_simplifier.h b/src/library/tactic/defeq_simplifier/defeq_simplifier.h
index 86121c641c..ee69dd15b6 100644
--- a/src/library/tactic/defeq_simplifier/defeq_simplifier.h
+++ b/src/library/tactic/defeq_simplifier/defeq_simplifier.h
@@ -10,6 +10,7 @@ Author: Daniel Selsam
 
 namespace lean {
 expr defeq_simplify(type_context & ctx, defeq_simp_lemmas const & simp_lemmas, expr const & e);
+expr defeq_simplify(type_context & ctx, expr const & e);
 void initialize_defeq_simplifier();
 void finalize_defeq_simplifier();
 }