`extract_goal`

: Format the current goal as a stand-alone example #

Useful for testing tactics or creating minimal working examples.

```
example (i j k : Nat) (h₀ : i ≤ j) (h₁ : j ≤ k) : i ≤ k := by
extract_goal
/-
theorem extracted_1 (i j k : Nat) (h₀ : i ≤ j) (h₁ : j ≤ k) : i ≤ k := sorry
-/
```

- TODO: Add tactic code actions?
- Output may produce lines with more than 100 characters

### Caveat #

Tl;dr: sometimes, using `set_option [your pp option] in extract_goal`

may work where `extract_goal`

does not.

The extracted goal may depend on imports and `pp`

options, since it relies on delaboration.
For this reason, the extracted goal may not be equivalent to the given goal.
However, the tactic responds to pretty printing options.
For example, calling `set_option pp.all true in extract_goal`

in the examples below actually works.

```
-- `theorem int_eq_nat` is the output of the `extract_goal` from the example below
-- the type ascription is removed and the `↑` is replaced by `Int.ofNat`:
-- Lean infers the correct (false) statement
theorem int_eq_nat {z : Int} : ∃ n, Int.ofNat n = z := sorry
example {z : Int} : ∃ n : Nat, ↑n = z := by
extract_goal -- produces `int_eq_nat`
apply int_eq_nat -- works
```

However, importing `Std.Classes.Cast`

, makes `extract_goal`

produce a different theorem

```
import Std.Classes.Cast
-- `theorem extracted_1` is the output of the `extract_goal` from the example below
-- the type ascription is erased and the `↑` is untouched:
-- Lean infers a different statement, since it fills in `↑` with `id` and uses `n : Int`
theorem extracted_1 {z : Int} : ∃ n, ↑n = z := ⟨_, rfl⟩
example {z : Int} : ∃ n : Nat, ↑n = z := by
extract_goal
apply extracted_1
/-
tactic 'apply' failed, failed to unify
∃ n, n = ?z
with
∃ n, ↑n = z
z: Int
⊢ ∃ n, ↑n = z
-/
```

Similarly, the extracted goal may fail to type-check:

```
example (a : α) : ∃ f : α → α, f a = a := by
extract_goal
exact ⟨id, rfl⟩
theorem extracted_1.{u_1} {α : Sort u_1} (a : α) : ∃ f, f a = a := sorry
-- `f` is uninterpreted: `⊢ ∃ f, sorryAx α true = a`
```

and also

```
import Mathlib.Data.Polynomial.Basic
-- The `extract_goal` below produces this statement:
theorem extracted_1 : X = X := sorry
-- Yet, Lean is unable to figure out what is the coefficients Semiring for `X`
/-
typeclass instance problem is stuck, it is often due to metavariables
Semiring ?m.28495
-/
example : (X : Nat[X]) = X := by
extract_goal
```

`extract_goal`

formats the current goal as a stand-alone theorem or definition,
and `extract_goal name`

uses the name `name`

instead of an autogenerated one.

It tries to produce an output that can be copy-pasted and just work, but its success depends on whether the expressions are amenable to being unambiguously pretty printed.

By default it cleans up the local context. To use the full local context, use `extract_goal*`

.

The tactic responds to pretty printing options.
For example, `set_option pp.all true in extract_goal`

gives the `pp.all`

form.