Lean4
/-- `pull` is the inverse tactic to `push`.
It pulls the given constant towards the head of the expression. For example
- `pull _ ∈ _` rewrites `x ∈ y ∨ ¬ x ∈ z` into `x ∈ y ∪ zᶜ`.
- `pull (disch := positivity) Real.log` rewrites `log a + 2 * log b` into `log (a * b ^ 2)`.
- `pull fun _ ↦ _` rewrites `f ^ 2 + 5` into `fun x => f x ^ 2 + 5` where `f` is a function.
A lemma is considered a `pull` lemma if its reverse direction is a `push` lemma
that actually moves the given constant away from the head. For example
- `not_or : ¬ (p ∨ q) ↔ ¬ p ∧ ¬ q` is a `pull` lemma, but `not_not : ¬ ¬ p ↔ p` is not.
- `log_mul : log (x * y) = log x + log y` is a `pull` lemma, but `log_abs : log |x| = log x` is not.
- `Pi.mul_def : f * g = fun (i : ι) => f i * g i` and `Pi.one_def : 1 = fun (x : ι) => 1` are both
`pull` lemmas for `fun`, because every `push fun _ ↦ _` lemma is also considered a `pull` lemma.
TODO: define a `@[pull]` attribute for tagging `pull` lemmas that are not `push` lemmas.
-/
@[tactic_parser 1000]
public meta def pull : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.Push.pull 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "pull" false✝)
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.discharger))
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
(ParserDescr.cat✝ `term 0)))
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.location))
