diff --git a/tests/lean/extra/goal_hole.lean b/tests/lean/extra/goal_hole.lean
new file mode 100644
index 000000000..d8a8a2b34
--- /dev/null
+++ b/tests/lean/extra/goal_hole.lean
@@ -0,0 +1,5 @@
+example (a b c : nat) : a = b → b = c → a = c :=
+begin
+  intro h₁ h₂,
+  exact eq.trans _ h₂
+end