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

def Mathlib.Tactic.extractGoal : Lean.ParserDescr

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.

Equations

• One or more equations did not get rendered due to their size.