Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The delta-deriving handler always makes instances defs even when their types are Props. This is inconsistent with the behavior of a handwritten instance.

For example:

def Foo (α : Type u) := List α

deriving instance Nonempty for Foo

/--
info: @[implicit_reducible] def instNonemptyFoo.{u_1} : ∀ (α : Type u_1), Nonempty (Foo α) :=
-/
#guard_msgs (substring := true) in
#print instNonemptyFoo

Context

This was observed in leanprover-community/batteries#1727, which updates the defLemma linter (identifying definitions which are Props and so should be theorems) to remove workarounds for #2575 now that #2575 has been fixed.

Steps to Reproduce

1. Create a type synonym Foo.
2. Invoke deriving instance MyProp for Foo where MyProp is a Prop class.

Expected behavior: The created instance is a theorem/.thmInfo.

Actual behavior: The created instance is a def/.defnInfo

Versions

Lean 4.31.0-nightly-2026-04-06

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.