have tr': a < b ∨ b < a ∨ a = b  := by permutateOr tr, [0, 2, 1]
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a > b
tr : a < b ∨ a = b ∨ b < a
⊢ a = b
α : Type
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a > b
tr : a < b ∨ a = b ∨ b < a
tr' : a < b ∨ b < a ∨ a = b
⊢ a = b