no goals
α : Type u_1
β✝ : Type ?u.19348
inst✝¹ : LinearOrder α
x y : α
β : Type u_2
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ cmp y x = cmp y' x'
rwa [← cmp_swap x', ← cmp_swap, swap_inj]
no goals
α : Type u_1
β✝ : Type ?u.19348
inst✝¹ : LinearOrder α
x y : α
β : Type u_2
inst✝ : LinearOrder β
x' y' : β
h : cmp y x = cmp y' x'
⊢ cmp x y = cmp x' y'
rwa [← cmp_swap y', ← cmp_swap, swap_inj]