Lean 4

Use the project's pinned toolchain and the bundled references to produce Lean code that elaborates, compiles, and preserves the intended theorem or program semantics.

Establish the project context

Before changing code:

1. Inspect lean-toolchain, lakefile.toml or lakefile.lean, lake-manifest.json, the target file's imports, and nearby declarations.
2. Treat the pinned Lean and Mathlib versions as authoritative. Do not upgrade a toolchain, dependency, or import set unless the request requires it.
3. Follow the repository's namespace, declaration, tactic, formatting, and import conventions.
4. Determine whether the task concerns core Lean, Mathlib, an educational dialect with custom tactics, or project-specific definitions.

Work against Lean's feedback

Validate names, types, and proof states instead of relying on memory.