multi-hole-with-helpers regression example

multi_hole_helpers_example — a formalization challenge from the lean-eval benchmark.

Notes

Regression test for trusted-helper support in multi-hole problems. Exercises three failure modes the generator used to have: (1) helpers at root namespace (rootHelper) must not get a spurious open; (2) the helper namespace Helpers differs from the module's last path component MultiHoleHelpersExample, so the injected open must be derived from the helper names rather than the module name; (3) the helper Helpers.postHole appears in source order between two holes, exercising the right-to-left edit pass against a layout where a sequential strip-then-replace pipeline (with helper ranges taken from .ilean and applied after hole-body replacement) would have shifted offsets. A submission that defines Submission.Helpers.first := 1, Submission.Helpers.second_eq := rfl, and Submission.Helpers.third_eq := rfl should be accepted.

• Holes (3): Helpers.first (def), Helpers.second_eq (theorem), Helpers.third_eq (theorem)

Formal statement

def first : Nat := sorry

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: Helpers.second_eq, Helpers.third_eq
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.