fix: use target type's instances in delta deriving

[kim-em]

Summary

When deriving an instance for a type alias (e.g., def ENat := WithTop ℕ), the instance-implicit class parameters in the derived instance TYPE were using instances synthesized for the UNDERLYING type, not the ALIAS type.

This caused a diamond when the alias has its own instance for a dependency class (e.g., AddMonoidWithOne from CommSemiring) that differs from the underlying type's instance (e.g., WithTop.addMonoidWithOne). Instance search would fail because it expected the alias's instance but the derived instance used the underlying's.

The fix: after synthesis succeeds, for each instance-implicit class parameter, re-synthesize for the target type and use that instance if it's defeq to what we synthesized for the underlying type.

Example

class MyBase (α : Type) where value : Nat := 42
class MyHigher (α : Type) [MyBase α] : Prop where prop : True

instance instBaseNat : MyBase Nat := {}
def MyAlias := Nat
instance instBaseMyAlias : MyBase MyAlias := {}  -- Different expression, but defeq

instance instHigherNat : MyHigher Nat where prop := trivial
deriving instance MyHigher for MyAlias

Before: instMyHigherMyAlias : @MyHigher MyAlias instBaseNat → instance search fails
After: instMyHigherMyAlias : @MyHigher MyAlias instBaseMyAlias → instance search succeeds

Motivation

This fixes the CharZero ℕ∞ diamond in Mathlib where the derived instance was using WithTop.addMonoidWithOne instead of the AddMonoidWithOne from CommSemiring ℕ∞, requiring set_option backward.isDefEq.respectTransparency false workarounds.

🤖 Prepared with Claude Code

[leanprover-bot]

Reference manual CI status:

• ✅ Reference manual branch lean-pr-testing-12339 has successfully built against this PR. (2026-02-06 06:47:38) View Log
• 🟡 Reference manual branch lean-pr-testing-12339 build against this PR didn't complete normally. (2026-02-06 06:49:25) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-12339 has successfully built against this PR. (2026-02-06 07:37:57) View Log