fix: preserve @[implicit_reducible] for WF-recursive definitions

[Copilot]

This PR fixes @[implicit_reducible] on well-founded recursive definitions.

addPreDefAttributes sets WF-recursive definitions as @[irreducible] by default, skipping this only when the user explicitly wrote @[reducible] or @[semireducible]. It was missing @[instance_reducible] and @[implicit_reducible], causing those attributes to be silently overridden.

Add instance_reducible and implicit_reducible to the check in src/Lean/Elab/PreDefinition/Mutual.lean that guards against overriding user-specified reducibility attributes, and add regression tests in tests/elab/wfirred.lean.

Example

-- Before fix: printed @[irreducible] def f : List Nat → Nat
-- After fix:  printed @[implicit_reducible] def f : List Nat → Nat
@[instance_reducible] def f : ∀ _l : List Nat, Nat
  | [] => 0
  | [_x] => 1
  | x :: y :: l => if h : x = y then f (x :: l) else f l + 2
termination_by l => sizeOf l

#print sig f

Fixes #12775

[nomeata]

@copilot looks good. Please reformat PR title and description according to the commit convention.

[Copilot]

@copilot looks good. Please reformat PR title and description according to the commit convention.

Updated the PR description to follow the commit convention. The PR title should be updated to: fix: preserve \@[instance_reducible]` for WF-recursive definitions`

[Rob23oba]

The new preferred name is @[implicit_reducible] so maybe use that instead in the title (also link #12775)