positivity: what it can and can't use from hypotheses (Mathlib v4.35.0)

positivity only closes goals of the form 0 < e, 0 ≤ e, or e ≠ 0. 1 ≤ x^2 + 1 gives 'not a positivity goal'; use have := sq_nonneg x; linarith there. For atoms it does look at local hypotheses: hx : 0 < x, hx : 1 < x, or hx : x ≠ 0 (for 0 < x^2) all work. But it does not chain them: from 0 < y and y ≤ x it can't get 0 < x, and from 0 < x it can't prove 0 < x - x/2, because subtraction is never handled (use linarith). 0 < Real.log x from hx : 1 < x fails, since the log extension only handles numerals like Real.log 2. Use Real.log_pos hx, or have := Real.log_pos hx first; then positivity accepts the term as an atom. Real.exp x, n.factorial, |x|, and even powers are handled.