fix: use target type's instances in delta deriving

[kim-em]

This PR fixes a diamond problem in delta deriving where instance-implicit class parameters in the derived instance type were using instances synthesized for the underlying type, not the alias type.

When deriving an instance for a type alias (e.g., def ENat := WithTop ℕ), 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 under #12179 where the derived instance was using WithTop.addMonoidWithOne instead of the AddMonoidWithOne from CommSemiring ℕ∞.

🤖 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
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-08 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-02-09 03:09:52)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-15-rev1 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-02-15 21:12:43)

[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
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-02-15-rev1 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-15 21:12:41)

[mathlib-lean-pr-testing]

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

[cursor]

Cursor Bugbot has reviewed your changes and found 2 potential issues.

^{Bugbot Autofix is OFF. To automatically fix reported issues with Cloud Agents, enable Autofix in the Cursor dashboard.}

This is the final PR Bugbot will review for you during this billing cycle

Your free Bugbot reviews will reset on March 11

Details

You are on the Bugbot Free tier. On this plan, Bugbot will review limited PRs each billing cycle.

To receive Bugbot reviews on all of your PRs, visit the Cursor dashboard to activate Pro and start your 14-day free trial.

[mathlib-lean-pr-testing]

• ✅ Mathlib branch lean-pr-testing-12339 has successfully built against this PR. (2026-02-16 00:35:47) View Log