Lean4
/-- Push negations into the conclusion or a hypothesis.
For instance, a hypothesis `h : ¬ ∀ x, ∃ y, x ≤ y` will be transformed by `push_neg at h` into
`h : ∃ x, ∀ y, y < x`. Binder names are preserved.
`push_neg` is a special case of the more general `push` tactic, namely `push Not`.
The `push` tactic can be extended using the `@[push]` attribute. `push` has special-casing
built in for `push Not`, so that it can preserve binder names, and so that `¬ (p ∧ q)` can be
transformed to either `p → ¬ q` (the default) or `¬ p ∨ ¬ q`. To get `¬ p ∨ ¬ q`, use
`set_option push_neg.use_distrib true`.
Another example: given a hypothesis
```lean
h : ¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε
```
writing `push_neg at h` will turn `h` into
```lean
h : ∃ ε > 0, ∀ δ > 0, ∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|
```
Note that binder names are preserved by this tactic, contrary to what would happen with `simp`
using the relevant lemmas. One can use this tactic at the goal using `push_neg`,
at every hypothesis and the goal using `push_neg at *` or at selected hypotheses and the goal
using say `push_neg at h h' ⊢`, as usual.
-/
@[tactic_parser 1000]
public meta def push_neg : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.Push.push_neg 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "push_neg" false✝)
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.location))
