`.brecOn` theorem is not marked as aux recursor

Prerequisites

Please put an X between the brackets as you perform the following steps:

• 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

On Prop-valued inductives, .brecOn is not marked as an aux recursor according to Lean.isAuxRecursor.

Context

I noticed this while trying to filter out definitions which are aux recursors.

Steps to Reproduce

import Lean

inductive Ex1 : Prop where
  | next : Ex1 → Ex1

inductive Ex2 : Type where
  | next : Ex2 → Ex2

-- compare with `.casesOn`
/--
info: true
-/
#guard_msgs in
run_meta do IO.println <| Lean.isAuxRecursor (← Lean.getEnv) ``Ex1.casesOn
/--
info: true
-/
#guard_msgs in
run_meta do IO.println <| Lean.isAuxRecursor (← Lean.getEnv) ``Ex2.casesOn


/--
info: false
-/
#guard_msgs in
run_meta do IO.println <| Lean.isAuxRecursor (← Lean.getEnv) ``Ex1.brecOn
/--
info: true
-/
#guard_msgs in
run_meta do IO.println <| Lean.isAuxRecursor (← Lean.getEnv) ``Ex2.brecOn

-- this could be consistent, and is not a limitation of how aux recursors work
run_cmd Lean.modifyEnv fun env => Lean.markAuxRecursor env ``Ex1.brecOn

/--
info: true
-/
#guard_msgs in
run_meta do IO.println <| Lean.isAuxRecursor (← Lean.getEnv) ``Ex1.brecOn

Expected behavior: All the run_metas output true

Actual behavior: there is inconsistency

Versions

• Lean 4.19.0-rc2
  Target: x86_64-unknown-linux-gnu
• Lean 4.18.0-rc1
  Target: x86_64-w64-windows-gnu Windows
• Lean 4.20.0-nightly-2025-04-05
  Target: x86_64-unknown-linux-gnu
• Lean 4.18.0
  Target: x86_64-unknown-linux-gnu

Additional Information

This could be related to the fact that Ex1.brecOn is a theorem but Ex2.brecOn is a def.

Impact

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

Start with the minimal reproduction using Lean.isAuxRecursor, Ex1.brecOn, Ex2.brecOn, and Lean.markAuxRecursor. Compare how the aux-recursor marking differs for Prop- and Type-valued inductives, including the theorem-versus-def distinction noted in the issue. Done means the supplied checks consistently report true without manual marking.