fix: make delta-derived Prop-valued instances theorems

This PR makes the delta-deriving handler create `theorem` declarations
instead of `def` declarations when the instance type is a `Prop`.
Previously, `deriving instance Nonempty for Foo` would always create a
`def`, which is inconsistent with the behavior of a handwritten
`instance` declaration.

Closes #13295

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

src/Lean/Elab/Deriving/Basic.lean

@@ -233,25 +233,33 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
         finally
           Core.setMessageLog (msgLog ++ (← Core.getMessageLog))
   let env ← getEnv
-  let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
-  let decl ← mkDefinitionValInferringUnsafe instName result.levelParams.toList result.type result.value hints
-  -- Pre-check: if the instance value depends on noncomputable definitions and the user didn't write
-  -- `noncomputable`, give an actionable error with a `Try this:` suggestion.
-  unless isNoncomputable || (← read).isNoncomputableSection || (← isProp result.type) do
-    let noncompRef? := preNormValue.foldConsts none fun n acc =>
-      acc <|> if Lean.isNoncomputable (asyncMode := .local) env n then some n else none
-    if let some noncompRef := noncompRef? then
-      if let some cmdRef := cmdRef? then
-        if let some origText := cmdRef.reprint then
-          let newText := (origText.replace "deriving instance " "deriving noncomputable instance ").trimAscii
-          logInfoAt cmdRef m!"Try this: {newText}"
-      throwError "failed to derive instance because it depends on \
-        `{.ofConstName noncompRef}`, which is noncomputable"
-  if isNoncomputable || (← read).isNoncomputableSection then
-    addDecl <| Declaration.defnDecl decl
-    modifyEnv (addNoncomputable · instName)
+  let isPropType ← isProp result.type
+  if isPropType then
+    let decl ← mkThmOrUnsafeDef {
+      name := instName, levelParams := result.levelParams.toList,
+      type := result.type, value := result.value
+    }
+    addDecl decl
   else
-    addAndCompile <| Declaration.defnDecl decl
+    let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
+    let decl ← mkDefinitionValInferringUnsafe instName result.levelParams.toList result.type result.value hints
+    -- Pre-check: if the instance value depends on noncomputable definitions and the user didn't write
+    -- `noncomputable`, give an actionable error with a `Try this:` suggestion.
+    unless isNoncomputable || (← read).isNoncomputableSection do
+      let noncompRef? := preNormValue.foldConsts none fun n acc =>
+        acc <|> if Lean.isNoncomputable (asyncMode := .local) env n then some n else none
+      if let some noncompRef := noncompRef? then
+        if let some cmdRef := cmdRef? then
+          if let some origText := cmdRef.reprint then
+            let newText := (origText.replace "deriving instance " "deriving noncomputable instance ").trimAscii
+            logInfoAt cmdRef m!"Try this: {newText}"
+        throwError "failed to derive instance because it depends on \
+          `{.ofConstName noncompRef}`, which is noncomputable"
+    if isNoncomputable || (← read).isNoncomputableSection then
+      addDecl <| Declaration.defnDecl decl
+      modifyEnv (addNoncomputable · instName)
+    else
+      addAndCompile <| Declaration.defnDecl decl
   trace[Elab.Deriving] "Derived instance `{.ofConstName instName}`"
   registerInstance instName AttributeKind.global (eval_prio default)
   addDeclarationRangesFromSyntax instName (← getRef)

tests/elab/derivingDelta.lean

@@ -380,3 +380,22 @@ deriving instance NCP for NCPAlias
 
 /-- info: instNCPNCPAlias -/
 #guard_msgs in #synth NCP NCPAlias
+
+/-!
+Prop-valued instances should be `theorem`s, not `def`s (issue #13295).
+-/
+def Foo (α : Type u) := List α
+deriving instance Nonempty for Foo
+
+/--
+info: @[implicit_reducible] theorem instNonemptyFoo.{u_1} : ∀ (α : Type u_1), Nonempty (Foo α) :=
+fun α => instNonemptyFoo._proof_1 α
+-/
+#guard_msgs in #print instNonemptyFoo
+
+-- NCP is Prop-valued, so its derived instance should also be a theorem.
+/--
+info: @[implicit_reducible] theorem instNCPNCPAlias : NCP NCPAlias :=
+instNCPNCPAlias._proof_1
+-/
+#guard_msgs in #print instNCPNCPAlias

tests/elab/deriving_diamond_defeq.lean

@@ -81,7 +81,7 @@ set_option pp.all true in
 #check @instMyHigherMyAlias
 
 /--
-info: @[implicit_reducible] def instMyHigherMyAlias : @MyHigher MyAlias instBaseMyAlias :=
+info: @[implicit_reducible] theorem instMyHigherMyAlias : @MyHigher MyAlias instBaseMyAlias :=
 instMyHigherMyAlias._proof_1
 -/
 #guard_msgs in