diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index b91434e58..0b67083d0 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -213,7 +213,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const &
             } else {
                 throw parser_error("invalid 'have' tactic, 'by', 'begin', 'proof', or 'from' expected", p.pos());
             }
-        } else if (p.curr_is_token(get_show_tk()) ||
+        } else if (p.curr_is_token(get_show_tk()) || p.curr_is_token(get_match_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();
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index 82a3bb4d5..bcc8ab108 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -53,6 +53,7 @@ static name * g_assert       = nullptr;
 static name * g_assume       = nullptr;
 static name * g_take         = nullptr;
 static name * g_fun          = nullptr;
+static name * g_match        = nullptr;
 static name * g_ellipsis     = nullptr;
 static name * g_raw          = nullptr;
 static name * g_true         = nullptr;
@@ -176,6 +177,7 @@ void initialize_tokens() {
     g_assume       = new name("assume");
     g_take         = new name("take");
     g_fun          = new name("fun");
+    g_match        = new name("match");
     g_ellipsis     = new name("...");
     g_raw          = new name("raw");
     g_true         = new name("true");
@@ -329,6 +331,7 @@ void finalize_tokens() {
     delete g_wf;
     delete g_all_transparent;
     delete g_ellipsis;
+    delete g_match;
     delete g_fun;
     delete g_take;
     delete g_assume;
@@ -424,6 +427,7 @@ name const & get_assert_tk() { return *g_assert; }
 name const & get_assume_tk() { return *g_assume; }
 name const & get_take_tk() { return *g_take; }
 name const & get_fun_tk() { return *g_fun; }
+name const & get_match_tk() { return *g_match; }
 name const & get_ellipsis_tk() { return *g_ellipsis; }
 name const & get_raw_tk() { return *g_raw; }
 name const & get_true_tk() { return *g_true; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index f107aa3f9..4e91816b9 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -55,6 +55,7 @@ name const & get_assert_tk();
 name const & get_assume_tk();
 name const & get_take_tk();
 name const & get_fun_tk();
+name const & get_match_tk();
 name const & get_ellipsis_tk();
 name const & get_raw_tk();
 name const & get_true_tk();
diff --git a/tests/lean/run/match_tac.lean b/tests/lean/run/match_tac.lean
new file mode 100644
index 000000000..e16ce6837
--- /dev/null
+++ b/tests/lean/run/match_tac.lean
@@ -0,0 +1,19 @@
+import data.nat
+
+example (a b c : Prop) : a ∧ b ↔ b ∧ a :=
+begin
+  apply iff.intro,
+  {intro H,
+   match H with
+   |  and.intro H₁ H₂ := and.intro H₂ H₁
+   end},
+  {intro H,
+   match H with
+   | and.intro H₁ H₂ := and.intro H₂ H₁
+   end},
+end
+
+open nat
+
+example : ∀ (a b : nat), a = b → b = a
+| a a rfl := rfl