nlinarith is a proof automation that attempts to finish a proof using the simplex method to find a linear combination of hypotheses and things that have already been proven, as well as some quadratic terms of them.

Docs: https://leanprover-community.github.io/mathlib4_docs/Mathlib...