diff --git a/tests/lean/run/pendingInstBug.lean b/tests/lean/run/pendingInstBug.lean
new file mode 100644
index 0000000000..a99999fa94
--- /dev/null
+++ b/tests/lean/run/pendingInstBug.lean
@@ -0,0 +1,8 @@
+class AddIdepotent (α : Type u) [Add α] : Prop where
+  add_id (x : α) : x + x = x
+
+export AddIdepotent (add_id)
+
+theorem tst [Add α] [AddIdepotent α] (x : α) : id (x + x + x)  = x := by
+  rw [add_id, add_id]
+  simp [id]