Add perf tests for projections of expensive structs

[nomeata]

This adds two perf tests about how a checker compares two projections, a.i =?= b.i, whose structs are expensive to evaluate.

• perf/proj-cheap-struct: (S u).re = (S ()).re, where reducing S _ to a constructor takes Θ(2^17) steps. Official keeps the structs stuck during definitional equality (whnf_core with cheap_proj) and finds them equal by their arguments, with five unfoldings in all. A checker that fully reduces a projection's struct evaluates S on both sides.
• perf/proj-lazy-struct: (P (slow 100000)).1 = (Q (slow 100001)).1, where P a and Q a both unfold to (0, a). The structs differ but the first fields agree. Official unfolds the structs lazily and projects as soon as neither side unfolds any further (lazy_delta_proj_reduction), with four unfoldings. A checker that compares the structs completely before projecting also evaluates the differing second fields.

The first test is distilled from a Palomar submission (roos-j/lean-spherical) that the con-ron bundled with Lean v4.35.0-rc3 failed with "fuel exhausted: whnf loop", while nanoda and official accepted it. There the structs are Finset.sums over Finset.range (2^17) under Complex.re. The second test is a regression that a first attempt at fixing con-leche introduced. A fix has to pass both tests.

Local results:

	proj-cheap-struct	proj-lazy-struct
official, lean4lean, mathgraph, nanoclo(-fortran), eink0rn, ind-models	✅	✅
nanoda, nanobruijn	✅	✅ (~7.8 s)
rpylean	✅ (12.5 s)	✅
con-leche, con-ron	error: fuel exhausted	✅
kiota	✅	decline (WHNF depth limit)
vow-lean-kernel	✅	error (stack overflow)
canonical-min	decline	reject
evmlean	timeout	✅ (3.4 s)
overfull	timeout	timeout

A con-leche fix that mirrors official's is_def_eq_core is on the way, and a con-ron port of it is in progress.

🤖 Generated with Claude Code

https://claude.ai/code/session_01XWm1rSWq3gU3E9qWjqPQup