diff --git a/tests/lean/elab10.lean b/tests/lean/elab10.lean
index 5c6378deef..54857838cb 100644
--- a/tests/lean/elab10.lean
+++ b/tests/lean/elab10.lean
@@ -13,3 +13,8 @@ attribute int_comm_ring [instance]
 #elab int → int
 
 #elab ((λ x, x + 1) : int → int)
+
+#elab λ (A : Type) (a b c d : A) (H1 : a = b) (H2 : b = c) (H3 : d = c),
+     have a = c, from eq.trans H1 H2,
+     have H3' : c = d, from eq.symm H3,
+     show a = d, from eq.trans this H3'
diff --git a/tests/lean/elab10.lean.expected.out b/tests/lean/elab10.lean.expected.out
index 568d6107b2..2fd1e02840 100644
--- a/tests/lean/elab10.lean.expected.out
+++ b/tests/lean/elab10.lean.expected.out
@@ -7,3 +7,8 @@ int → int : Type
   @add int (@distrib.to_has_add int (@ring.to_distrib int (@comm_ring.to_ring int int_comm_ring))) x
     (@one int (@monoid.to_has_one int (@ring.to_monoid int (@comm_ring.to_ring int int_comm_ring)))) :
   int → int
+λ (A : Type) (a b c d : A) (H1 : @eq A a b) (H2 : @eq A b c) (H3 : @eq A d c),
+  have this : @eq A a c, from @eq.trans A a b c H1 H2,
+  have H3' : @eq A c d, from @eq.symm A d c H3,
+  show @eq A a d, from @eq.trans A a c d this H3' :
+  ∀ (A : Type) (a b c d : A), @eq A a b → @eq A b c → @eq A d c → @eq A a d