diff --git a/tests/lean/951.lean b/tests/lean/951.lean
new file mode 100644
index 0000000000..b107b0c87d
--- /dev/null
+++ b/tests/lean/951.lean
@@ -0,0 +1,17 @@
+inductive ThingA where
+| mkA
+deriving Ord
+instance : LE ThingA where
+  le a b := (compare a b).isLE
+
+instance (t₁ t₂ : ThingA) : Decidable (t₁ <= t₂) := inferInstance
+-- TODO: we may want to suppress the name of nested instances
+#check instDecidableLeThingAInstLEThingA
+
+inductive ThingB where
+| mkB
+deriving Ord
+instance : LE ThingB where
+  le a b := (compare a b).isLE
+instance (t₁ t₂ : ThingB) : Decidable (t₁ <= t₂) := inferInstance
+#check instDecidableLeThingBInstLEThingB
diff --git a/tests/lean/951.lean.expected.out b/tests/lean/951.lean.expected.out
new file mode 100644
index 0000000000..62f2c8e85d
--- /dev/null
+++ b/tests/lean/951.lean.expected.out
@@ -0,0 +1,2 @@
+instDecidableLeThingAInstLEThingA : (t₁ t₂ : ThingA) → Decidable (t₁ ≤ t₂)
+instDecidableLeThingBInstLEThingB : (t₁ t₂ : ThingB) → Decidable (t₁ ≤ t₂)