diff --git a/tests/lean/cond_tac.lean b/tests/lean/cond_tac.lean
new file mode 100644
index 000000000..dbdd86820
--- /dev/null
+++ b/tests/lean/cond_tac.lean
@@ -0,0 +1,45 @@
+import tactic
+(*
+simple_tac = Cond(function(env, ios, s)
+                     local gs = s:goals()
+                     local n, g = gs:head()
+                     local r = g:conclusion():is_and()
+                     print ("Cond result: " .. tostring(r))
+                     return r
+                  end,
+                  Then(apply_tac("and_intro"), assumption_tac()),
+                  Then(apply_tac("or_introl"), assumption_tac()))
+
+simple2_tac = When(function(env, ios, s)
+                      local gs = s:goals()
+                      local n, g = gs:head()
+                      local r = g:conclusion():is_and()
+                      print ("When result: " .. tostring(r))
+                      return r
+                   end,
+                   apply_tac("and_intro"))
+*)
+theorem T1 (a b c : Bool) : a -> b -> c -> a ∧ b.
+  (* simple_tac *)
+  done
+
+theorem T2 (a b : Bool) : a -> a ∨ b.
+  (* simple_tac *)
+  done
+
+definition x := 10
+theorem T3 : x + 20 +2 >= 2*x.
+  (* eval_tac() *)
+  (* trivial_tac() *)
+  done
+
+theorem T4 (a b c : Bool) : a -> b -> c -> a ∧ b.
+  (* simple2_tac *)
+  exact
+  done
+
+theorem T5 (a b c : Bool) : a -> b -> c -> a ∨ b.
+  (* simple2_tac *)
+  apply or_introl
+  exact
+  done
diff --git a/tests/lean/cond_tac.lean.expected.out b/tests/lean/cond_tac.lean.expected.out
new file mode 100644
index 000000000..0646e0988
--- /dev/null
+++ b/tests/lean/cond_tac.lean.expected.out
@@ -0,0 +1,13 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'tactic'
+Cond result: true
+  Proved: T1
+Cond result: false
+  Proved: T2
+  Defined: x
+  Proved: T3
+When result: true
+  Proved: T4
+When result: false
+  Proved: T5