feat: split [implicit_reducible] into [instance_reducible] and [implicit_reducible] tiers

[kim-em]

This PR splits TransparencyMode.instances and ReducibilityStatus.implicitReducible into two tiers so that user-written @[implicit_reducible] annotations no longer "corrupt" type class search.

The transparency hierarchy is now none < reducible < instances < implicit < default < all:

• .instances (TC tier, semantically narrowed): unfolds [reducible] and the new [instance_reducible] constants. Used during type class synthesis.
• .implicit (new tier): also unfolds user-written [implicit_reducible]. Used when checking definitional equality of implicit value arguments.

ReducibilityStatus correspondingly gains instanceReducible. The instance command, mutual data-instance defaults, and subobject class projections auto-stamp .instanceReducible. Match auxiliaries are also .instanceReducible so type class synthesis can unfold them. The user-facing @[instance_reducible] attribute (formerly an alias for @[implicit_reducible]) is repurposed to set this status; an instance_reducible -> implicit_reducible upgrade transition is allowed for users who want both tiers.

Existing core constants previously tagged @[implicit_reducible] (e.g. Nat.add, Array.size, maxOfLe/minOfLe, integer comparisons, ring auxiliaries, well-founded relations) have been migrated to @[instance_reducible] to preserve TC behavior. Mathlib can now use the narrower @[implicit_reducible] for functors etc. without affecting type class search.

The withImplicitConfig helper is split into withInstanceConfig (TC-tier) and withImplicitConfig (implicit-arg-defeq tier). Per-site callers route to the appropriate tier: instance-implicit [..] arguments and class-projection struct args use withInstanceConfig; other implicit args under implicitBump and checkTypesAndAssign use withImplicitConfig. The @[defeq] rfl simp-theorem admission check moves to .implicit to match the broader contract simp uses; Generalize.kabstract and reduceCtorEq similarly use .implicit to preserve their pre-split behavior.

Sites previously using isImplicitReducible as a proxy for "is an instance / support symbol" (grind MBTC, grind Internalize, simp/grind locals filters, library suggestions, dup-namespace linter, several LCNF heuristics) now use the new isInstanceReducible predicate, which is a precise tag post-split.

The transparency bit-packing in Config.toKey has been widened from 2 bits to 3 bits to accommodate the sixth constructor; all subsequent field offsets shift by 1.

TransparencyMode.implicit is appended at the end of the inductive (out of unfolding order) to preserve existing constructor indices, matching the existing convention noted on TransparencyMode (constructors are not in unfolding order to avoid bootstrapping pain).

A new regression test in tests/elab/splitImplicitReducible.lean pins the new contract.

🤖 Prepared with Claude Code

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ea6e76707835317858b7dd36c95322679c50aaac --onto dae325700c89e23c453b1d6d5ed5432d87880062. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-06 02:45:50)
• 💥 Mathlib branch lean-pr-testing-13637 build failed against this PR. (2026-05-06 04:02:58) View Log
• 💥 Mathlib branch lean-pr-testing-13637 build failed against this PR. (2026-05-08 07:30:48) View Log

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase ea6e76707835317858b7dd36c95322679c50aaac --onto 3fc99eef102549c743c6c63547983319bfae6f01. You can force reference manual CI using the force-manual-ci label. (2026-05-06 02:45:51)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-05-04 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-05-06 03:57:12)
• 🟡 Reference manual branch lean-pr-testing-13637 build against this PR didn't complete normally. (2026-05-08 07:30:40) View Log
• 💥 Reference manual branch lean-pr-testing-13637 build failed against this PR. (2026-05-08 07:30:54) View Log