Lean4
/-- `push` pushes the given constant away from the head of the expression. For example
- `push _ ∈ _` rewrites `x ∈ {y} ∪ zᶜ` into `x = y ∨ ¬ x ∈ z`.
- `push (disch := positivity) Real.log` rewrites `log (a * b ^ 2)` into `log a + 2 * log b`.
- `push ¬ _` is the same as `push_neg` or `push Not`, and it rewrites
`¬ ∀ ε > 0, ∃ δ > 0, δ < ε` into `∃ ε > 0, ∀ δ > 0, ε ≤ δ`.
In addition to constants, `push` can be used to push `fun` and `∀` binders:
- `push fun _ ↦ _` rewrites `fun x => f x ^ 2 + 5` into `f ^ 2 + 5`
- `push ∀ _, _` rewrites `∀ a, p a ∧ q a` into `(∀ a, p a) ∧ (∀ a, q a)`.
The `push` tactic can be extended using the `@[push]` attribute.
To instead move a constant closer to the head of the expression, use the `pull` tactic.
To push a constant at a hypothesis, use the `push ... at h` or `push ... at *` syntax.
-/
@[tactic_parser 1000]
public meta def push : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.Push.push 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "push" 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))
