Partial order less than antisymmetry

Stream: Is there code for X?

[Eric Paul]

I often find myself in a situation like the following and this is my goto way to solve it. However, it takes more mental effort than I feel like should be required and so am wondering if there is an easier way:

import Mathlib

example {α : Type*} [PartialOrder α] {a b : α} (a_lt_b : a < b) (b_lt_a : b < a) : 2 < 1 := by
  exact False.elim ((lt_self_iff_false a).mp (gt_trans b_lt_a a_lt_b))

[Matt Diamond]

personally I would just do (a_lt_b.not_lt b_lt_a).elim

[Matt Diamond]

you could also do (lt_asymm a_lt_b b_lt_a).elim

[Eric Paul]

Those are both a fair bit simpler, thank you!

[Yakov Pechersky]

docs#absurd is also good for such situations

[Yakov Pechersky]

exact absurd a_lt_b b_lt_a.not_lt. or even simp [b_lt_a.not_lt] at a_lt_b for more complex situations

[Zhang Qinchuan]

After using absurd the goal can be closed by the output of exact?.

import Mathlib

example {α : Type*} [PartialOrder α] {a b : α} (a_lt_b : a < b) (b_lt_a : b < a) : 2 < 1 := by
  absurd a_lt_b
  -- `exact?` gives the following:
  exact not_lt_of_gt b_lt_a

[Violeta Hernández]

You can also replace False.elim by cases False if you want

[Eric Paul]

All great suggestions, thanks for the help. It’s super useful seeing all the different perspectives.

[Eric Paul]

As an update, thanks to Vasilii Nesterov, I can now just do

import Mathlib

example {α : Type*} [PartialOrder α] {a b : α} (a_lt_b : a < b) (b_lt_a : b < a) : 2 < 1 := by
  order