diff --git a/tests/lean/run/quotInd.lean b/tests/lean/run/quotInd.lean
new file mode 100644
index 0000000000..f620e29cd7
--- /dev/null
+++ b/tests/lean/run/quotInd.lean
@@ -0,0 +1,3 @@
+example (r : α → α → Prop) (q : Quot r) : False := by
+  induction q using Quot.ind with
+  | mk x => admit