variable-binder minimal example

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

Notes

Regression for https://github.com/leanprover/lean-eval/issues/276. The theorem inherits implicit binders from a preceding variable declaration, which the extractor must re-emit in the generated workspace.

Formal statement

theorem variable_binder_example
    (A : Matrix n n ℚ) (hA : A.IsHermitian) :
    A.trace = ∑ i, A i i := by
  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: variable_binder_example
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.