perf: make the `Expr` hash combinator a bijection in each argument

This PR fixes a quadratic slowdown in the kernel when checking terms that contain long chains of the same application, such as `"ff…f" = String.ofList (List.replicate n 'f')`.

`Expr` stores a 32-bit hash. The hash of `f a` was the low 32 bits of `mixHash` applied to the data of `f` and `a`. Truncating to 32 bits makes the map from the hash of `a` to the hash of `f a` non-injective. Iterating such a map, as in `f a`, `f (f a)`, `f (f (f a))`, ..., enters a cycle after about 2^16 steps on average (13,146 cells for `'f'`). From then on, chains of different lengths share hashes, each lookup in the kernel caches compares them structurally, and the check becomes quadratic.

This PR adds `mixHash32 : UInt32 → UInt32 → UInt32`, based on the block step of `MurmurHash3_x86_32`. With either argument fixed, it is a bijection in the other. `Expr.data` now uses it to combine the hashes of subterms. Then `hash (fⁿ a) = hash (fⁿ⁺ᵏ a)` implies `hash a = hash (fᵏ a)`, so the chain can only repeat by returning to the hash of `a`, which takes about 2^31 steps on average. The PR also:
* gives `lam` and `forallE` distinct tags; before, `fun x : A => b` and `∀ x : A, b` always had the same hash,
* includes the `nondep` flag of `letE` in its hash, and
* no longer mixes `approxDepth` into the hash.

Instructions for the kernel check of `"ff…f" = String.ofList (List.replicate n 'f')` (excluding `import Lean`):

| n | Before | After |
|---|---|---|
| 10,000 | 1.07G | 1.07G |
| 20,000 | 7.22G | 2.14G |
| 40,000 | 201.4G | 4.28G |
| 80,000 | 2,746G | 8.56G |
| 160,000 | <timeout> | 17.1G |
| 320,000 | <timeout> | 34.2G |

On Mathlib, the change costs +0.08% instructions, with no change in memory.

We are considering increasing the `Expr` hash to 64 bits. That would make accidental collisions negligible, but it adds 8 bytes to every `Expr` node. On Mathlib, this increases the total size of the `.olean` files by 17% (+984 MB), memory use by about 3.5%, and CPU time by about 1%.

Closes #16103

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>