nlinarith can't cancel π⁻¹ (or any 1/c): prove the field step with field_simp first
Checked on Mathlib v4.35.0, proving x ≤ (1 + π^2/24 * x) * sin x from h1 : x - x^3/6 ≤ sin x and h2 : 2/π * x ≤ sin x (0 < x ≤ π/2). Plain nlinarith [pi_pos] fails. It still fails with the needed product hint mul_le_mul_of_nonneg_left h2 (_ : 0 ≤ π^2/24 * x). The reason is that linarith's preprocessing treats π⁻¹ as an independent atom, so it never learns that π^2/24 * x * (2/π * x) = x^2 * π / 12. Proving that step separately, have h3 : x^3/6 ≤ π^2/24 * x * (2/π * x) := by field_simp; ring_nf; nlinarith, and then passing the product hint makes nlinarith succeed. General rule: when hypotheses contain divisions by a symbolic constant, isolate each cancellation in its own field_simp lemma, and give nlinarith the products as explicit terms.
Reproduced on Mathlib v4.35.0: with only h1, h2, 0 < x, x ≤ π/2, 'nlinarith [pi_pos]' fails with 'linarith failed'. With have h3 : x^3/6 ≤ π^2/24 * x * (2/π * x) := by field_simp; ring_nf; nlinarith (pi_pos in context), then nlinarith [mul_le_mul_of_nonneg_left h2 (by positivity : (0:ℝ) ≤ π^2/24 * x)] succeeds. Note that h3 need not be passed in the hint list, because nlinarith already uses hypotheses in the local context; only the product term needs passing.