no goals
cmp✝ : ?m.3864 → ?m.3864 → Ordering
inst✝² : TransCmp cmp✝
x✝ : Sort u_1
cmp : x✝ → x✝ → Ordering
inst✝¹ : TransCmp cmp
y z x : x✝
inst✝ : TransCmp cmp
yz : cmp y z = Ordering.eq
⊢ cmp x y = cmp x z
rw [← Ordering.swap_inj, symm, symm, cmp_congr_left yz]