perf: inline dependent instances into specialized decls

[zwarich]

No description provided.

[zwarich]

!bench

[leanprover-bot]

Here are the benchmark results for commit b4f9997.
There were significant changes against commit 17f76f3:

  Benchmark                              Metric                 Change
  ===========================================================================================
+ Init.Data.BitVec.Lemmas                branches                -3.2%              (-67.0 σ)
+ Init.Data.BitVec.Lemmas                instructions            -3.2%              (-59.9 σ)
+ Init.Data.List.Sublist async           branches                -4.1%             (-139.0 σ)
+ Init.Data.List.Sublist async           instructions            -4.1%             (-124.3 σ)
+ Init.Prelude async                     branches                -2.2%             (-283.6 σ)
+ Init.Prelude async                     instructions            -2.3%             (-261.7 σ)
+ Std.Data.DHashMap.Internal.RawLemmas   branch-misses           -4.9%              (-39.5 σ)
+ Std.Data.DHashMap.Internal.RawLemmas   branches                -2.9%             (-172.3 σ)
+ Std.Data.DHashMap.Internal.RawLemmas   instructions            -3.0%             (-155.4 σ)
+ Std.Data.Internal.List.Associative     branches                -4.0%             (-337.8 σ)
+ Std.Data.Internal.List.Associative     instructions            -4.1%             (-298.9 σ)
+ big_do                                 branches                -5.4%            (-6785.9 σ)
+ big_do                                 instructions            -5.6%            (-4740.7 σ)
+ big_match                              branch-misses           -2.3%              (-23.3 σ)
+ big_match                              branches                -1.2%             (-159.1 σ)
+ big_match                              instructions            -1.2%             (-131.7 σ)
+ big_omega.lean                         branches                -3.8%             (-316.9 σ)
+ big_omega.lean                         instructions            -3.6%             (-398.9 σ)
+ big_omega.lean MT                      branches                -3.8%             (-212.1 σ)
+ big_omega.lean MT                      instructions            -3.6%             (-243.9 σ)
+ bv_decide_inequality.lean              task-clock              -1.2%             (-107.6 σ)
+ bv_decide_mul                          branches                -1.2%             (-126.3 σ)
+ bv_decide_mul                          instructions            -1.1%              (-90.9 σ)
+ bv_decide_realworld                    branches                -2.2%             (-105.9 σ)
+ bv_decide_realworld                    instructions            -2.0%              (-86.5 σ)
+ bv_decide_rewriter.lean                branch-misses           -5.6%              (-25.7 σ)
+ bv_decide_rewriter.lean                branches                -3.4%             (-211.0 σ)
+ bv_decide_rewriter.lean                instructions            -3.6%             (-237.6 σ)
+ channel.lean                           unbounded_seq           -1.8%
+ channel.lean                           unbounded_spsc          -2.0% (-117669558323691.0 σ)
+ grind_bitvec2.lean                     branches                -2.3%             (-240.2 σ)
+ grind_bitvec2.lean                     instructions            -2.3%             (-216.0 σ)
+ grind_list2.lean                       branches                -2.6%             (-109.7 σ)
+ grind_list2.lean                       instructions            -2.7%              (-99.0 σ)
+ grind_ring_5.lean                      branches                -1.3%              (-52.0 σ)
+ grind_ring_5.lean                      instructions            -1.2%              (-42.1 σ)
+ iterators                              branches               -19.8%            (-9603.1 σ)
+ iterators                              instructions           -16.3%            (-8005.5 σ)
+ iterators                              task-clock             -18.4%              (-34.4 σ)
+ iterators                              wall-clock             -18.9%              (-43.3 σ)
+ lake config elab                       instructions            -2.4%              (-86.2 σ)
+ mut_rec_wf                             branch-misses           -2.5%              (-20.2 σ)
+ mut_rec_wf                             branches                -1.4%             (-162.7 σ)
+ mut_rec_wf                             instructions            -1.3%             (-135.6 σ)
+ omega_stress.lean async                branches                -1.8%             (-154.1 σ)
+ omega_stress.lean async                instructions            -1.7%             (-105.5 σ)
+ simp_bubblesort_256                    branches                -5.6%             (-192.1 σ)
+ simp_bubblesort_256                    instructions            -5.8%             (-166.5 σ)
+ simp_local                             branches                -1.8%             (-226.9 σ)
+ simp_local                             instructions            -1.9%             (-193.7 σ)
+ simp_subexpr                           branch-misses           -6.4%              (-88.9 σ)
+ simp_subexpr                           branches                -5.5%             (-489.8 σ)
+ simp_subexpr                           instructions            -5.7%             (-767.3 σ)
+ stdlib                                 instructions            -3.2%             (-129.0 σ)
+ stdlib                                 longest rebuild path    -2.9%              (-46.0 σ)
+ workspaceSymbols with new ranges       branches                -2.1%             (-124.2 σ)
+ workspaceSymbols with new ranges       instructions            -2.2%             (-114.1 σ)

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 17f76f3bd7b22c95a08a2dd2e6372dbc42602000 --onto 21f5263f2f28e5fd7b6a99c40f0c11351f04aedb. You can force Mathlib CI using the force-mathlib-ci label. (2025-08-23 17:11:45)

[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 17f76f3bd7b22c95a08a2dd2e6372dbc42602000 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-08-23 17:11:46)