positivity — Mathlib

Lean4
/-- Tactic solving goals of the form `0 ≤ x`, `0 < x` and `x ≠ 0`.  The tactic works recursively
according to the syntax of the expression `x`, if the atoms composing the expression all have
numeric lower bounds which can be proved positive/nonnegative/nonzero by `norm_num`.  This tactic
either closes the goal or fails.

Examples:
```
example {a : ℤ} (ha : 3 < a) : 0 ≤ a ^ 3 + a := by positivity

example {a : ℤ} (ha : 1 < a) : 0 < |(3:ℤ) + a| := by positivity

example {b : ℤ} : 0 ≤ max (-3) (b ^ 2) := by positivity
```
-/
@[tactic_parser 1000]
public meta def positivity : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.Positivity.positivity 1024 (ParserDescr.nonReservedSymbol✝ "positivity" false✝)
Похожие утверждения