Lean4
/-- An extension of `linarith` with some preprocessing to allow it to solve some nonlinear arithmetic
problems. (Based on Coq's `nra` tactic.) See `linarith` for the available syntax of options,
which are inherited by `nlinarith`; that is, `nlinarith!` and `nlinarith only [h1, h2]` all work as
in `linarith`. The preprocessing is as follows:
* For every subterm `a ^ 2` or `a * a` in a hypothesis or the goal,
the assumption `0 ≤ a ^ 2` or `0 ≤ a * a` is added to the context.
* For every pair of hypotheses `a1 R1 b1`, `a2 R2 b2` in the context, `R1, R2 ∈ {<, ≤, =}`,
the assumption `0 R' (b1 - a1) * (b2 - a2)` is added to the context (non-recursively),
where `R ∈ {<, ≤, =}` is the appropriate comparison derived from `R1, R2`.
-/
@[tactic_parser 1000]
public meta def nlinarith : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.nlinarith 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "nlinarith" false✝)
(ParserDescr.unary✝ `optional (ParserDescr.symbol✝ "!")))
Mathlib.Tactic.linarithArgsRest)
