feat: improve #print recursor rules

[kmill]

This PR improves the way #print describes recursors. For example, #print Nat.rec now gives the following:

recursor Nat.rec.{u} {motive : Nat → Sort u} (zero : motive Nat.zero) (succ : (n : Nat) → motive n → motive n.succ)
  (t : Nat) : motive t
number of parameters: 0
number of motives: 1 (position 1)
number of minor premises: 2 (positions 2–3)
number of indices: 0
major premise position: 4
rules:
  Nat.rec zero succ Nat.zero
    ==> zero
  Nat.rec zero succ n.succ
    ==> succ n (Nat.rec zero succ n)

For reference, the Nat.rec rules were formerly printed as

rules:
for Nat.zero (0 fields): fun motive zero succ => zero
for Nat.succ (1 fields): fun motive zero succ n => succ n (Nat.rec zero succ n)

These are the raw lambda expressions that the kernel uses to evaluate the reductions. For the new output, we construct the logical reduction rules instead. This is especially helpful in understanding the reduction rules of auxiliary recursors for nested inductive types (i.e. T.rec_1, T.rec_2, ...).

The recursor's type signature is also now pretty printed using named binders like #check, given the importance of the binder names.

This builds on #10543.

With @berberman

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-25 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-28 20:34:20)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-14960 has successfully built against this PR. (2026-08-28 21:32:48) View Log