# Documentation

Mathlib.Tactic.ExtractGoal

# 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.

Instances For