diff --git a/tests/lean/run/focus.lean b/tests/lean/run/focus.lean
new file mode 100644
index 0000000000..2032cfa07d
--- /dev/null
+++ b/tests/lean/run/focus.lean
@@ -0,0 +1,12 @@
+open nat
+example (n m : ℕ) : n + m = m + n :=
+begin
+  induction m with m IHm,
+  focus { induction n with n IHn,
+    focus { reflexivity },
+    focus { exact congr_arg succ IHn }},
+  focus { apply eq.trans (congr_arg succ IHm),
+    clear IHm, induction n with n IHn,
+    focus { reflexivity },
+    focus { exact congr_arg succ IHn }}
+end
\ No newline at end of file