Inline lambda bodies into comprehensions; emit set comprehensions

[emeryberger]

Summary

Improves the fidelity of Python comprehensions generated from Lean list operations.

• List comprehensions now inline the lambda body. xs.map (fun x => x + 1) produces [x + 1 for x in xs] instead of a helper def + [_f(x) for x in xs]. Covers map, filter, filterMap, bind(flatMap), any, all, find?, findSome?.
• Set comprehensions are new. List.eraseDups / .toFinset / .toSet emit {x for x in xs} instead of list(dict.fromkeys(...)), and fuse an upstream map/filter: (xs.filter (·>5)).eraseDups → {x for x in xs if 5 < x}, with the dead intermediate line removed.

Behavior that is deliberately preserved

• A named or caller-supplied function argument (xs.map f, xs.map Nat.succ) still emits correctly — Nat.succ inlines to n + 1, an unknown f stays [f(x) for x in xs].
• A lambda whose body is not a simple expression (e.g. if/else) falls back to a real def — never a call to an undefined name.
• A deferred lambda used as a plain value is re-materialized as (lambda p: e).

How it works

In LCNF a map lambda lowers to a local def the combinator references by name. emitLocalFun now tries to render a single-parameter lambda's body as one Python expression (renderExprCode/renderLetValueExpr); on success it defers the lambda (records (param, body), emits no def), rolling back all state on failure. Comprehension combinators splice the body in via fnCompParts. The renderer is conservative — it returns none for anything not in a known-safe set (constructors, OfNat, bne, nested cases/fun), so those lambdas fall back to a correct def.

See CLAUDE.md → "Lambda Inlining Architecture" for details.

Testing

• New Comprehensions.lean + Comprehensions_test.py: asserts both semantics (correct output) and structure (inlining actually happens, complex bodies fall back to a def, dedup produces a set comprehension, no stale dict.fromkeys).
• Corpus regression: F821 = 201, F811 = 37 — identical to the pre-change baseline (verified via ruff over the full Corpus/CorpusTestCombined.lean output).
• New GitHub Actions CI workflow (.github/workflows/ci.yml) builds the library and runs both the comprehension and Bool-branch/min-max regression suites on every push and PR.