scicraft/LeanCat huggingface dataset:
You are an expert in Lean 4 and Mathematics. Please finish the following proof in Lean4 code.
Do not change the original statement. Copy the final statement to prove exactly.
Please include the complete header, including imports and namespaces, 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.

The statement for you to complete is:

```lean4
{formal_statement}
```