# Extract Have Statements to Lemmas

This tool is deprecated and will be removed in a future release.

Use [extract_decls](https://axle.axiommath.ai/extract_decls) instead, which supports all declaration kinds.

## Input

**environment***  
Lean environment or version  
`lean-4.32.0`, `lean-4.31.0`, `lean-4.30.0`, `lean-4.29.0`, `lean-4.28.0`, `lean-4.27.0`, `lean-4.26.0`, `lean-4.25.1`, `lean-4.24.0`, `lean-4.23.0`, `lean-4.22.0`, `lean-4.21.0`

**ignore_imports**  
Ignore import mismatches

Default header (injected when enabled):  
```
import Mathlib
```

**content***  
Lean source code

**names**  
Theorem names to process

**indices**  
Theorem indices to process

**theorems_only**  
Process theorems/lemmas only

**include_have_body**  
Include proof bodies in extracted lemmas

**include_whole_context**  
Include whole context when extracting

**reconstruct_callsite**  
Replace have statement with lemma call

**verbosity**  
Pretty-printer verbosity level (0-2)

**timeout_seconds**  
Max execution time in seconds

RUNCLEAR

## Result

Shareable Link

API Call

FILE A BUG