diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 54e0b9b78c..0bb73b6744 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -38,6 +38,7 @@ Author: Leonardo de Moura
 #include "library/projection.h"
 #include "library/private.h"
 #include "library/decl_stats.h"
+#include "library/app_builder.h"
 #include "library/meng_paulson.h"
 #include "library/definitional/projection.h"
 #include "library/simplifier/simp_rule_set.h"
@@ -1138,6 +1139,28 @@ static environment relevant_thms_cmd(parser & p) {
     return env;
 }
 
+static environment app_builder_cmd(parser & p) {
+    environment const & env = p.env();
+    type_checker tc(env);
+    app_builder b(tc);
+    name c = p.check_constant_next("invalid #app_builder command, constant expected");
+    p.check_token_next(get_lparen_tk(), "invalid #app_builder command, '(' expected");
+    buffer<expr> args;
+    while (true) {
+        args.push_back(p.parse_expr());
+        if (!p.curr_is_token(get_comma_tk()))
+            break;
+        p.next();
+    }
+    p.check_token_next(get_rparen_tk(), "invalid #app_builder command, ')' expected");
+    if (auto r = b.mk_app(c, args.size(), args.data())) {
+        p.regular_stream() << *r << "\n";
+    } else {
+        p.regular_stream() << "<failed>\n";
+    }
+    return env;
+}
+
 void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("open",           "create aliases for declarations, and use objects defined in other namespaces",
                         open_cmd));
@@ -1161,6 +1184,7 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("#erase_cache",   "erase cached definition (for debugging purposes)", erase_cache_cmd));
     add_cmd(r, cmd_info("#projections",   "generate projections for inductive datatype (for debugging purposes)", projections_cmd));
     add_cmd(r, cmd_info("#telescope_eq",  "(for debugging purposes)", telescope_eq_cmd));
+    add_cmd(r, cmd_info("#app_builder",   "(for debugging purposes)", app_builder_cmd));
     add_cmd(r, cmd_info("#compile",       "(for debugging purposes)", compile_cmd));
     add_cmd(r, cmd_info("#accessible",    "(for debugging purposes) display number of accessible declarations for blast tactic", accessible_cmd));
     add_cmd(r, cmd_info("#decl_stats",    "(for debugging purposes) display declaration statistics", decl_stats_cmd));
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index b23dded19b..3f2c792d2f 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -119,7 +119,7 @@ void init_token_table(token_table & t) {
          "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
          "multiple_instances", "find_decl", "attribute", "persistent",
          "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq",
-         "#compile", "#accessible", "#decl_stats", "#relevant_thms", nullptr};
+         "#compile", "#accessible", "#decl_stats", "#relevant_thms", "#app_builder", nullptr};
 
     pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},
diff --git a/tests/lean/run/app_builder.lean b/tests/lean/run/app_builder.lean
new file mode 100644
index 0000000000..78747f17e4
--- /dev/null
+++ b/tests/lean/run/app_builder.lean
@@ -0,0 +1,18 @@
+import algebra.ring
+
+variables a b c : nat
+variables H1 : a = b
+variables H2 : b = c
+set_option pp.all true
+
+#app_builder eq.refl (a)
+#app_builder eq.trans (H1, H2)
+#app_builder eq.symm (H1)
+
+open algebra
+variables A : Type
+variables [s : comm_ring A]
+variables x y : A
+
+#app_builder eq.refl (s)
+#app_builder eq.refl (x)