fix: opacify functions using {Expr,Level}.data

[digama0]

This PR is a follow-up to #8554, and the fixes #8559, #8560 for it. These fixed the main issue, but currently it is still possible to prove that the functions cannot be correct because they involve projecting out of a finite type. This fixes the issue without any performance impact by changing all the defs that use Expr.Data to opaque (as suggested here), so we can soundly assume as an axiom that the functions are implemented correctly. This will unblock lean4lean.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-05-31 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. (2025-06-16 22:52:21)