scicraft/LeanCat huggingface dataset:
You are an expert in Lean 4 and Mathematics. Please finish the following proof in Lean4 code.
If provided a formal statement, do not change it. Include the complete header so that your code can pass the Lean4 compiler.
You may introduce auxiliary definitions, instances, and lemmas before the target statement if needed. The target statement and all auxiliary code must contain no sorry, admit, axiom, or unsafe declarations.

Natural language statement:
{nl_statement}

Lean 4 formal statement:
{formal_statement}

Reference knowledge from Mathlib search:
{search_contents}