diff --git a/tests/lean/run/hcongr_1.lean b/tests/lean/run/hcongr_1.lean
new file mode 100644
index 0000000000..f50943e295
--- /dev/null
+++ b/tests/lean/run/hcongr_1.lean
@@ -0,0 +1,6 @@
+import data.tuple
+
+#hcongr @tuple.append
+#hcongr @add
+#hcongr @list.ith
+#hcongr (@list.ith nat)