Commit 2024-08-06 23:04 48415a3e

feat(Tactic.Bound): Add a bound tactic for inequalities by structure (#10562) bound proves inequalities that follow "obviously by structure", assuming nonnegativity or positivity of subterms where necessary. It is built on top of Aesop. It has significant overlap with positivity and gcongr, but can also switch back and forth between those modes (such as when proving 0 < a * b - a * c from 0 < a, c < b). Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/.60bound.60.20mixes.20.60gcongr.60.20and.20.60positivity.60/near/412120380