variable-binder minimal example

variable_binder_example

Submitter: Kim Morrison.

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.

Source: Unavailable.

Informal solution: Unavailable.

theorem declaration uses `sorry`variable_binder_example (A : Matrix n n ℚ) (hA : A.IsHermitian) :
    A.trace = ∑ i, A i i := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℚhA:A.IsHermitian⊢ A.trace = ∑ i, A i i
  sorryAll goals completed! 🐙

Solved by

• @LorenzoLuccioli with Aristotle (Harmonic) on May 22, 2026 (proof)

• @rishistyping with Stealth Model on May 24, 2026