diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index eeba1a6d8..83ded9f5b 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -143,7 +143,7 @@ static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
     return p.mk_by(t, pos);
 }
 
-static expr parse_begin_end_core(parser & p, pos_info const & pos) {
+static expr parse_begin_end_core(parser & p, pos_info const & pos, name const & end_token, bool nested = false) {
     if (!p.has_tactic_decls())
         throw parser_error("invalid 'begin-end' expression, tactic module has not been imported", pos);
     environment env = open_tactic_namespace(p);
@@ -153,7 +153,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
     optional<expr> pre_tac = get_begin_end_pre_tactic(env);
     buffer<expr> tacs;
     bool first = true;
-    while (!p.curr_is_token(get_end_tk())) {
+    while (!p.curr_is_token(end_token)) {
         if (first) {
             first = false;
         } else {
@@ -164,19 +164,27 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
                 tacs.push_back(mk_begin_end_element_annotation(info_tac));
             }
         }
-        if (p.curr_is_token(get_end_tk()))
+        if (p.curr_is_token(get_begin_tk())) {
+            auto pos = p.pos();
+            tacs.push_back(parse_begin_end_core(p, pos, get_end_tk(), true));
+        } else if (p.curr_is_token(get_lcurly_tk())) {
+            auto pos = p.pos();
+            tacs.push_back(parse_begin_end_core(p, pos, get_rcurly_tk(), true));
+        } else if (p.curr_is_token(end_token)) {
             break;
-        bool use_exact = (p.curr_is_token(get_have_tk()) || p.curr_is_token(get_show_tk()) ||
-                          p.curr_is_token(get_assume_tk()) || p.curr_is_token(get_take_tk()) ||
-                          p.curr_is_token(get_fun_tk()));
-        auto pos = p.pos();
-        expr tac = p.parse_expr();
-        if (use_exact)
-            tac = p.mk_app(get_exact_tac_fn(), tac, pos);
-        if (pre_tac)
-            tac = p.mk_app({get_and_then_tac_fn(), *pre_tac, tac}, pos);
-        tac = mk_begin_end_element_annotation(tac);
-        tacs.push_back(tac);
+        } else {
+            bool use_exact = (p.curr_is_token(get_have_tk()) || p.curr_is_token(get_show_tk()) ||
+                              p.curr_is_token(get_assume_tk()) || p.curr_is_token(get_take_tk()) ||
+                              p.curr_is_token(get_fun_tk()));
+            auto pos = p.pos();
+            expr tac = p.parse_expr();
+            if (use_exact)
+                tac = p.mk_app(get_exact_tac_fn(), tac, pos);
+            if (pre_tac)
+                tac = p.mk_app({get_and_then_tac_fn(), *pre_tac, tac}, pos);
+            tac = mk_begin_end_element_annotation(tac);
+            tacs.push_back(tac);
+        }
     }
     auto end_pos = p.pos();
     p.next();
@@ -196,11 +204,15 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
     for (unsigned i = 1; i < tacs.size(); i++) {
         r = p.mk_app({get_and_then_tac_fn(), r, tacs[i]}, end_pos);
     }
-    return p.mk_by(mk_begin_end_annotation(r), end_pos);
+    r = p.save_pos(mk_begin_end_annotation(r), end_pos);
+    if (nested)
+        return r;
+    else
+        return p.mk_by(r, end_pos);
 }
 
 static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & pos) {
-    return parse_begin_end_core(p, pos);
+    return parse_begin_end_core(p, pos, get_end_tk());
 }
 
 static expr parse_proof_qed_core(parser & p, pos_info const & pos) {
@@ -220,7 +232,7 @@ static expr parse_proof(parser & p, expr const & prop) {
         return parse_proof_qed_core(p, pos);
     } else if (p.curr_is_token(get_begin_tk())) {
         auto pos = p.pos();
-        return parse_begin_end_core(p, pos);
+        return parse_begin_end_core(p, pos, get_end_tk());
     } else if (p.curr_is_token(get_by_tk())) {
         // parse: 'by' tactic
         auto pos = p.pos();
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index eecc420c5..cf9996e13 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1536,6 +1536,9 @@ bool elaborator::try_using(substitution & subst, expr const & mvar, proof_state
 static void extract_begin_end_tactics(expr pre_tac, buffer<expr> & pre_tac_seq) {
     if (is_begin_end_element_annotation(pre_tac)) {
         pre_tac_seq.push_back(get_annotation_arg(pre_tac));
+    } else if (is_begin_end_annotation(pre_tac)) {
+        // nested begin-end block
+        pre_tac_seq.push_back(pre_tac);
     } else {
         buffer<expr> args;
         if (get_app_args(pre_tac, args) == get_and_then_tac_fn()) {
@@ -1548,47 +1551,64 @@ static void extract_begin_end_tactics(expr pre_tac, buffer<expr> & pre_tac_seq)
     }
 }
 
-void elaborator::try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac) {
+bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac) {
     lean_assert(is_begin_end_annotation(pre_tac));
     buffer<expr> pre_tac_seq;
     extract_begin_end_tactics(get_annotation_arg(pre_tac), pre_tac_seq);
     for (expr ptac : pre_tac_seq) {
-        expr new_ptac = subst.instantiate_all(ptac);
-        if (auto tac = pre_tactic_to_tactic(new_ptac)) {
-            try {
-                proof_state_seq seq = (*tac)(env(), ios(), ps);
-                auto r = seq.pull();
-                if (!r) {
-                    // tactic failed to produce any result
-                    display_unsolved_proof_state(mvar, ps, "tactic failed", ptac);
-                    return;
-                }
-                if (m_ctx.m_flycheck_goals) {
-                    if (auto p = pip()->get_pos_info(ptac)) {
-                        auto out = regular(env(), ios());
-                        flycheck_information info(out);
-                        if (info.enabled()) {
-                            display_information_pos(out, pip()->get_file_name(), p->first, p->second);
-                            out << " proof state:\n" << ps.pp(env(), ios()) << "\n";
+        if (is_begin_end_annotation(ptac)) {
+            goals gs = ps.get_goals();
+            if (!gs)
+                throw_elaborator_exception("invalid nested begin-end block, there are no goals to be solved", ptac);
+            goal  g   = head(gs);
+            expr mvar = g.get_mvar();
+            proof_state focus_ps(ps, goals(g));
+            if (!try_using_begin_end(subst, mvar, focus_ps, ptac))
+                return false;
+            substitution ps_new_subst = ps.get_subst();
+            name const & mvar_name    = mlocal_name(mvar);
+            ps_new_subst.assign(mvar_name, *subst.get_expr(mvar_name));
+            ps = proof_state(ps, tail(gs), ps_new_subst);
+        } else {
+            expr new_ptac = subst.instantiate_all(ptac);
+            if (auto tac = pre_tactic_to_tactic(new_ptac)) {
+                try {
+                    proof_state_seq seq = (*tac)(env(), ios(), ps);
+                    auto r = seq.pull();
+                    if (!r) {
+                        // tactic failed to produce any result
+                        display_unsolved_proof_state(mvar, ps, "tactic failed", ptac);
+                        return false;
+                    }
+                    if (m_ctx.m_flycheck_goals) {
+                        if (auto p = pip()->get_pos_info(ptac)) {
+                            auto out = regular(env(), ios());
+                            flycheck_information info(out);
+                            if (info.enabled()) {
+                                display_information_pos(out, pip()->get_file_name(), p->first, p->second);
+                                out << " proof state:\n" << ps.pp(env(), ios()) << "\n";
+                            }
                         }
                     }
+                    ps = r->first;
+                } catch (tactic_exception & ex) {
+                    display_tactic_exception(ex, ps, ptac);
+                    return false;
                 }
-                ps = r->first;
-            } catch (tactic_exception & ex) {
-                display_tactic_exception(ex, ps, ptac);
-                return;
+            } else {
+                return false;
             }
-        } else {
-            return;
         }
     }
 
     if (!empty(ps.get_goals())) {
         display_unsolved_proof_state(mvar, ps, "unsolved subgoals", pre_tac);
+        return false;
     } else {
         subst = ps.get_subst();
         expr v = subst.instantiate(mvar);
         subst.assign(mlocal_name(mvar), v);
+        return true;
     }
 }
 
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 13a55e0ec..e30227ac0 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -150,7 +150,7 @@ class elaborator : public coercion_info_manager {
     optional<tactic> pre_tactic_to_tactic(expr const & pre_tac);
     bool try_using(substitution & subst, expr const & mvar, proof_state const & ps,
                    expr const & pre_tac, tactic const & tac, bool show_failure);
-    void try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac);
+    bool try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac);
     void solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited);
     expr solve_unassigned_mvars(substitution & subst, expr e, name_set & visited);
     expr solve_unassigned_mvars(substitution & subst, expr const & e);
diff --git a/tests/lean/run/nested_begin_end.lean b/tests/lean/run/nested_begin_end.lean
new file mode 100644
index 000000000..470c79692
--- /dev/null
+++ b/tests/lean/run/nested_begin_end.lean
@@ -0,0 +1,29 @@
+example (p q : Prop) : p ∧ q ↔ q ∧ p :=
+begin
+apply iff.intro,
+  begin
+     intro H,
+     apply and.intro,
+     apply (and.elim_right H),
+     apply (and.elim_left H)
+  end,
+  begin
+    intro H,
+    apply and.intro,
+    apply (and.elim_right H),
+    apply (and.elim_left H)
+  end
+end
+
+example (p q : Prop) : p ∧ q ↔ q ∧ p :=
+begin
+apply iff.intro,
+  {intro H,
+   apply and.intro,
+   apply (and.elim_right H),
+   apply (and.elim_left H)},
+  {intro H,
+   apply and.intro,
+   apply (and.elim_right H),
+   apply (and.elim_left H)}
+end