fix: interaction between cbv_opaque and inline

[wkrozowski]

This PR fixes the interaction between cbv_opaque and inline/always_inline annotations, to make sure that inlined definitions marked as cbv_opaque are not unfolded during the preprocessing stage of cbv tactic.

[wkrozowski]

!bench

[leanprover-radar]

Benchmark results for d54e103 against 4ba85ac are in. There are no significant changes. @wkrozowski

• 🟥 build//instructions: +1.3G (+0.01%)

Small changes (3🟥)

• 🟥 build/module/Lean.Meta.Tactic.Cbv.Main//instructions: +1.7G (+12.73%) (reduced significance based on *//lines)
• 🟥 lake/inundation/config tree//task-clock: +12ms (+8.15%)
• 🟥 lake/inundation/config tree//wall-clock: +13ms (+8.32%)

[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 4ba85acc464e380c03034763e93506f695ae68d7 --onto 61a3443a9569d548a235f785b9a33984bb7ff622. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-19 11:39:27)

[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 4ba85acc464e380c03034763e93506f695ae68d7 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-19 11:39:29)