diff --git a/tests/lean/run/tactic1.lean b/tests/lean/run/tactic1.lean
index df08958608..b62cb04c7f 100644
--- a/tests/lean/run/tactic1.lean
+++ b/tests/lean/run/tactic1.lean
@@ -44,3 +44,18 @@ by {
   exact h₁;
   exact h₃
 }
+
+theorem ex7 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z :=
+by {
+  have y = z by apply Eq.symm; assumption;
+  apply Eq.trans;
+  exact h₁;
+  assumption
+}
+
+theorem ex8 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z :=
+by apply Eq.trans h₁;
+   have y = z by
+     apply Eq.symm;
+     assumption;
+   exact this