How to express "precisely one of ... holds?"

Stream: new members

[Adam Dingle]

Is there some nice way in Lean to say "Precisely one of these statements holds"?

For example, suppose I want to say that "precisely one of a < b, a = b, a > b holds". I could write

(a < b ∨ a = b ∨ a > b) ∧ ¬(a < b ∧ a = b) ∧ ¬(a = b ∧ a > b) ∧ ¬(a < b ∧ a > b)

but it seems unduly repetitive. Is there a nicer way?

[Eric Rodriguez]

You could use docs#Xor docs#Xor', but usually this just isn't done; for example, see docs#le_trichotomy

[Mauricio Collares]

Related thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Precisely.20one.20of.20these.20holds

[Adam Dingle]

Thanks for the helpful pointer - that other thread says it all. :)