Lean4
/-- 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 x y z ... h` 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 x₁ ... xₙ h` is `peel n e with x₁ ... xₙ h`.
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 x h'`
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ε N n hn h_peel` 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`.
-/
@[tactic_parser 1000]
public meta def peel : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.Peel.peel 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "peel" false✝)
(ParserDescr.unary✝ `optional (ParserDescr.const✝ `num)))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
(ParserDescr.cat✝ `term 0))))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " with")
(ParserDescr.unary✝ `many1
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
(ParserDescr.binary✝ `orelse (ParserDescr.const✝ `ident) (ParserDescr.const✝ `hole)))))))
(ParserDescr.unary✝ `optional Mathlib.Tactic.usingArg))
