ordering

Stream: new members

[Iocta]

I have a bunch of < and <= relations, and I want to combine them into a chain automatically, is there a tactic for this?

[Iocta]

ie all the lt_trans-like commands combined

[Bryan Gin-ge Chen]

You could write them in a calc block.

[Bryan Gin-ge Chen]

https://leanprover-community.github.io/extras/calc.html

[Reid Barton]

If you don't want to write the steps explicitly, linarith might work (not sure if it requires some extra structure on the ordering that you might not have but most likely do). I think mono might work as well.