linarith

Summary

The linarith tactic solves certain kind of linear equalities and inequalities. Unlike the ring tactic, linarith uses hypotheses in the tactic state.

You can feed extra proofs into linarith by adding them as a list like this: linarith [h1, h2]. We will see examples of this below.

Examples

To be written. Basically, if you have a bunch of hypotheses like h1 : a < b, h2 : b <= c, h3 : c = d and a goal of a < d then linarith will solve it; it knows a ton of results about how to put inequalities together. As another example if you have hypotheses h1 : a < b and h2 : c < d then it will prove a goal c + a < b + d.