# Extract Theorems

split file into separate theorems with dependencies (deprecated — use extract\_decls)

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):

```lean
import Mathlib
```

### content*

Lean source code

### names

Theorem names to process

### indices

Theorem indices to process

### timeout\_seconds

Max execution time in seconds