diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 22531ef72..a0d38699a 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -22,6 +22,8 @@ static name g_comma(",");
 static name g_fact("[fact]");
 static name g_from("from");
 static name g_using("using");
+static name g_then("then");
+static name g_have("have");
 static name g_by("by");
 
 static expr parse_Type(parser & p, unsigned, expr const *, pos_info const & pos) {
@@ -151,7 +153,7 @@ static void parse_have_modifiers(parser & p, bool & is_fact) {
     }
 }
 
-static expr parse_have(parser & p, unsigned, expr const *, pos_info const & pos) {
+static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> const & prev_local) {
     auto id_pos  = p.pos();
     bool is_fact = false;
     name id      = p.check_id_next("invalid 'have' declaration, identifier expected");
@@ -164,18 +166,41 @@ static expr parse_have(parser & p, unsigned, expr const *, pos_info const & pos)
         prop  = p.save_pos(mk_expr_placeholder(), id_pos);
     }
     p.check_token_next(g_comma, "invalid 'have' declaration, ',' expected");
-    expr proof = parse_proof(p, prop);
+    expr proof;
+    if (prev_local) {
+        parser::local_scope scope(p);
+        p.add_local(*prev_local);
+        auto proof_pos = p.pos();
+        proof = parse_proof(p, prop);
+        proof = p.save_pos(Fun(*prev_local, proof), proof_pos);
+        proof = p.save_pos(proof(*prev_local), proof_pos);
+    } else {
+        proof = parse_proof(p, prop);
+    }
     p.check_token_next(g_comma, "invalid 'have' declaration, ',' expected");
     parser::local_scope scope(p);
     expr l = p.save_pos(mk_local(id, prop), pos);
     binder_info bi = mk_contextual_info(is_fact);
     p.add_local(l, bi);
-    expr body  = abstract(p.parse_expr(), l);
+    expr body;
+    if (p.curr_is_token(g_then)) {
+        auto then_pos = p.pos();
+        p.next();
+        p.check_token_next(g_have, "invalid 'then have' declaration, 'have' expected");
+        body  = parse_have_core(p, then_pos, some_expr(l));
+    } else {
+        body  = p.parse_expr();
+    }
     // remark: mk_contextual_info(false) informs the elaborator that prop should not occur inside metavariables.
-    expr r     = p.save_pos(mk_lambda(id, prop, body, bi), pos);
+    body = abstract(body, l);
+    expr r = p.save_pos(mk_lambda(id, prop, body, bi), pos);
     return p.save_pos(mk_app(r, proof), pos);
 }
 
+static expr parse_have(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return parse_have_core(p, pos, none_expr());
+}
+
 static name H_show("H_show");
 static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) {
     expr prop  = p.parse_expr();
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 11df05cda..92b42d349 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -54,7 +54,7 @@ static char const * g_cup            = "\u2294";
 token_table init_token_table() {
     token_table t;
     std::pair<char const *, unsigned> builtin[] =
-        {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"by", 0},
+        {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"by", 0}, {"then", 0},
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {".{", 0}, {"Type", g_max_prec}, {"|", 0}, {"with", 0},
          {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0},
diff --git a/tests/lean/run/have3.lean b/tests/lean/run/have3.lean
new file mode 100644
index 000000000..1339fbb98
--- /dev/null
+++ b/tests/lean/run/have3.lean
@@ -0,0 +1,10 @@
+abbreviation Bool : Type.{1} := Type.{0}
+variables a b c : Bool
+axiom Ha : a
+axiom Hb : b
+axiom Hc : c
+check have H1 : a, from Ha,
+      then have H2 : a, from H1,
+      then have H3 : a, from H2,
+      then have H4 : a, from H3,
+      H4
\ No newline at end of file
diff --git a/tests/lean/run/have4.lean b/tests/lean/run/have4.lean
new file mode 100644
index 000000000..d6e170efa
--- /dev/null
+++ b/tests/lean/run/have4.lean
@@ -0,0 +1,10 @@
+abbreviation Bool : Type.{1} := Type.{0}
+variables a b c : Bool
+axiom Ha : a
+axiom Hb : b
+axiom Hc : c
+check have H1 : a, from Ha,
+      then have H2 : a, from H1,
+      have H3 : a, from H2,
+      then have H4 : a, from H3,
+      H4
\ No newline at end of file
diff --git a/tests/lean/run/have5.lean b/tests/lean/run/have5.lean
new file mode 100644
index 000000000..24d3c343a
--- /dev/null
+++ b/tests/lean/run/have5.lean
@@ -0,0 +1,11 @@
+abbreviation Bool : Type.{1} := Type.{0}
+variables a b c d : Bool
+axiom Ha : a
+axiom Hb : b
+axiom Hc : c
+print raw
+  have H1 : a, by skip,
+  then have H2 : b, by skip,
+  have H3 : c, by skip,
+  then have H4 : d, by skip,
+  H4
\ No newline at end of file