fix: zetaDelta := false regression

[leodemoura]

See new test. It is a mwe for an issue blocking Mathlib.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 47595540bbcd5ef218e60e11d6586589ff3788e1 --onto 6719af350fde9339354f28d091458df39a4af9d4. (2024-02-22 15:09:30)

[kmill]

Just recording here that it turns out that it turns out mathlib was relying on the sources in structure instance notation introducing local instances.

We're testing out a temporary workaround to have the spread syntax introduce let bindings itself, using a special let binder that changes the kind to be an implementation detail after introducing any local instances. (Spread syntax is that {...; __ := a; __ := b} is equivalent to {a, b with ...}. It's nice because it works with where syntax.) leanprover-community/mathlib4@77711ed