`deriving instance CoeFun/CoeSort` generates opaque aux constant for reducible type synonyms

Prerequisites

• 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

deriving instance CoeFun (and CoeSort) for a def synonym of a type that already has such an instance produces a derived instance whose field is wrapped in an opaque auxiliary constant, rather than referring to the original instance's field.

I believe this happens because the deriving handler's field-type check runs at instances transparency. If the synonym doesn't unfold at that transparency, the check fails, and the field is wrapped in an _aux_1 constant instead of being unfolded and reused directly. The wrapped field is opaque to simp, so simp lemmas about the original coercion (e.g. DFunLike.coe) no longer apply to the derived instance.

Context

While working on removing the set_option backward.inferInstanceAs.wrap.data false exceptions in mathlib4#42699, the only available workaround was tagging the synonym @[instance_reducible], which avoids the aux constant but makes the synonym unfold during all typeclass synthesis, not just this derivation, at a measurable build-time cost. As noted by @jcommelin on that PR, it would be preferable for the deriving handler to unfold the synonym internally while constructing the instance, rather than requiring a global reducibility change on the definition.

Steps to Reproduce

The following is a MWE by @b-mehta.

structure Wrap where
  f : Nat → Nat

instance : CoeFun Wrap fun _ => Nat → Nat := ⟨fun i ↦ i.f⟩

@[implicit_reducible] def N := Wrap
deriving instance CoeFun for N

#print instCoeFunNForallNat

Expected behavior: The derived instance's coe field refers directly to Wrap's CoeFun instance field.

Actual behavior: Even with @[implicit_reducible] on N, the field is wrapped in an opaque auxiliary constant, the output of
#print instCoeFunNForallNat:

@[instance_reducible] def instCoeFunNForallNat : CoeFun N fun x => Nat → Nat :=
{ coe := instCoeFunNForallNat._aux_1 }

Versions

4.35.0-nightly-2026-09-06

Additional Information

Only tagging N with @[instance_reducible] (not @[implicit_reducible]) avoids the aux constant.

Impact

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

Run the self-contained MWE with the Lean nightly release and inspect the deriving instance CoeFun and CoeSort handler, especially its field-type check. Compare the generated #print instCoeFunNForallNat output with the expected direct reference to the original CoeFun field; done means no opaque _aux_1 wrapper is generated without making N instance-reducible.