α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
x y : α✝
inst✝ : OrientedCmp cmp
⊢ cmp y x = Ordering.swap Ordering.eq ↔ cmp y x = Ordering.eq
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
x y : α✝
inst✝ : OrientedCmp cmp
⊢ cmp x y = Ordering.eq ↔ cmp y x = Ordering.eq
rw [← Ordering.swap_inj, symm]
no goals
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
x y : α✝
inst✝ : OrientedCmp cmp
⊢ cmp y x = Ordering.swap Ordering.eq ↔ cmp y x = Ordering.eq
exact .rfl