## Stream: new members

### Topic: ordering

#### Iocta (Jul 09 2020 at 04:51):

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

#### Iocta (Jul 09 2020 at 04:54):

ie all the lt_trans-like commands combined

#### Bryan Gin-ge Chen (Jul 09 2020 at 04:54):

You could write them in a calc block.

#### Bryan Gin-ge Chen (Jul 09 2020 at 04:55):

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

#### Reid Barton (Jul 09 2020 at 12:07):

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.

Last updated: May 17 2021 at 23:14 UTC