match cmp : compare x x with
| .eq => rfl
| .lt =>
  have h₁ : (compare x x).swap = .gt := by rw [cmp]; decide
  have h₂ : (compare x x).swap = .lt := by rw [symm]; assumption
  rw [h₂] at h₁
  contradiction
| .gt =>
  have h₁ : (compare x x).swap = .lt := by rw [cmp]; decide
  have h₂ : (compare x x).swap = .gt := by rw [symm]; assumption
  rw [h₂] at h₁
  contradiction
α : Type
inst✝ : Order α
x : α
⊢ compare x x = Ordering.eq
no goals