diff --git a/tests/lean/run/derivingInhabited.lean b/tests/lean/run/derivingInhabited.lean
new file mode 100644
index 0000000000..bfa452d582
--- /dev/null
+++ b/tests/lean/run/derivingInhabited.lean
@@ -0,0 +1,17 @@
+inductive Foo (α : Type u) (β : Type v) where
+  | mk₁ : α → Foo α β
+  | mk₂ : List β → Foo α β
+
+deriving instance Inhabited for Foo
+
+def ex1 : Inhabited (Foo α β) :=
+  inferInstance
+
+inductive Bla (α : Type u) (β : Type v) where
+  | mk₁ : α → Bla α β
+  | mk₂ : β → Bla α β
+
+deriving instance Inhabited for Bla
+
+def ex2 [Inhabited α] : Inhabited (Foo α β) :=
+  inferInstance