# The `peel`

tactic #

`peel h with h' idents*`

tries to apply `forall_imp`

(or `Exists.imp`

, or `Filter.Eventually.mp`

,
`Filter.Frequently.mp`

and `Filter.eventually_of_forall`

) with the argument `h`

and uses `idents*`

to introduce variables with the supplied names, giving the "peeled" argument the name `h'`

.

One can provide a numeric argument as in `peel 4 h`

which will peel 4 quantifiers off
the expressions automatically name any variables not specifically named in the `with`

clause.

In addition, the user may supply a term `e`

via `... using e`

in order to close the goal
immediately. In particular, `peel h using e`

is equivalent to `peel h; exact e`

. The `using`

syntax
may be paired with any of the other features of `peel`

.

Peels matching quantifiers off of a given term and the goal and introduces the relevant variables.

`peel e`

peels all quantifiers (at reducible transparency), using`this`

for the name of the peeled hypothesis.`peel e with h`

is`peel e`

but names the peeled hypothesis`h`

. If`h`

is`_`

then uses`this`

for the name of the peeled hypothesis.`peel n e`

peels`n`

quantifiers (at default transparency).`peel n e with h x y z ...`

peels`n`

quantifiers, names the peeled hypothesis`h`

, and uses`x`

,`y`

,`z`

, and so on to name the introduced variables; these names may be`_`

. If`h`

is`_`

then uses`this`

for the name of the peeled hypothesis. The length of the list of variables does not need to equal`n`

.`peel e with h x₁ ... xₙ`

is`peel n e with h x₁ ... xₙ`

.

There are also variants that apply to an iff in the goal:

`peel n`

peels`n`

quantifiers in an iff.`peel with x₁ ... xₙ`

peels`n`

quantifiers in an iff and names them.

Given `p q : ℕ → Prop`

, `h : ∀ x, p x`

, and a goal `⊢ : ∀ x, q x`

, the tactic `peel h with h' x`

will introduce `x : ℕ`

, `h' : p x`

into the context and the new goal will be `⊢ q x`

. This works
with `∃`

, as well as `∀ᶠ`

and `∃ᶠ`

, and it can even be applied to a sequence of quantifiers. Note
that this is a logically weaker setup, so using this tactic is not always feasible.

For a more complex example, given a hypothesis and a goal:

```
h : ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) < ε
⊢ ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) ≤ ε
```

(which differ only in `<`

/`≤`

), applying `peel h with h_peel ε hε N n hn`

will yield a tactic state:

```
h : ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) < ε
ε : ℝ
hε : 0 < ε
N n : ℕ
hn : N ≤ n
h_peel : 1 / (n + 1 : ℝ) < ε
⊢ 1 / (n + 1 : ℝ) ≤ ε
```

and the goal can be closed with `exact h_peel.le`

.
Note that in this example, `h`

and the goal are logically equivalent statements, but `peel`

*cannot* be immediately applied to show that the goal implies `h`

.

In addition, `peel`

supports goals of the form `(∀ x, p x) ↔ ∀ x, q x`

, or likewise for any
other quantifier. In this case, there is no hypothesis or term to supply, but otherwise the syntax
is the same. So for such goals, the syntax is `peel 1`

or `peel with x`

, and after which the
resulting goal is `p x ↔ q x`

. The `congr!`

tactic can also be applied to goals of this form using
`congr! 1 with x`

. While `congr!`

applies congruence lemmas in general, `peel`

can be relied upon
to only apply to outermost quantifiers.

Finally, the user may supply a term `e`

via `... using e`

in order to close the goal
immediately. In particular, `peel h using e`

is equivalent to `peel h; exact e`

. The `using`

syntax
may be paired with any of the other features of `peel`

.

This tactic works by repeatedly applying lemmas such as `forall_imp`

, `Exists.imp`

,
`Filter.Eventually.mp`

, `Filter.Frequently.mp`

, and `Filter.eventually_of_forall`

.

## Equations

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

## Instances For

The list of constants that are regarded as being quantifiers.

## Equations

- Mathlib.Tactic.Peel.quantifiers = [`Exists, `And, `Filter.Eventually, `Filter.Frequently]

## Instances For

If `unfold`

is false then do `whnfR`

, otherwise unfold everything that's not a quantifier,
according to the `quantifiers`

list.

## Equations

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

## Instances For

Throws an error saying `ty`

and `target`

could not be matched up.

## Equations

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

## Instances For

If `f`

is a lambda then use its binding name to generate a new hygienic name,
and otherwise choose a new hygienic name.

## Equations

- Mathlib.Tactic.Peel.mkFreshBinderName f = liftM (Lean.mkFreshUserName (match f with | Lean.Expr.lam n binderType body binderInfo => n | x => `a))

## Instances For

Applies a "peel theorem" with two main arguments, where the first is the new goal
and the second can be filled in using `e`

. Then it intros two variables with the
provided names.

If, for example, `goal : ∃ y : α, q y`

and `thm := Exists.imp`

, the metavariable returned has
type `q x`

where `x : α`

has been introduced into the context.

## Equations

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

## Instances For

This is the core to the `peel`

tactic.

It tries to match `e`

and `goal`

as quantified statements (using `∀`

and the quantifiers in
the `quantifiers`

list), then applies "peel theorems" using `applyPeelThm`

.

We treat `∧`

as a quantifier for sake of dealing with quantified statements
like `∃ δ > (0 : ℝ), q δ`

, which is notation for `∃ δ, δ > (0 : ℝ) ∧ q δ`

.

## Equations

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

## Instances For

Given a list `l`

of names, this peels `num`

quantifiers off of the expression `e`

and
the main goal and introduces variables with the provided names until the list of names is exhausted.
Note: the name `n?`

(with default `this`

) is used for the name of the expression `e`

with
quantifiers peeled.

## Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Tactic.Peel.peelArgs e 0 l n? unfold = pure PUnit.unit

## Instances For

Peel off a single quantifier from an `↔`

.

## Equations

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

## Instances For

Peel off quantifiers from an `↔`

and assign the names given in `l`

to the introduced
variables.

## Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Tactic.Peel.peelArgsIff [] = Lean.Elab.Tactic.withMainContext (pure ())