no goals
α : Type u_1
β✝ : Type ?u.20888
inst✝¹ : LinearOrder α
x y : α
β : Type u_2
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x = y ↔ x' = y'
rw [le_antisymm_iff, le_antisymm_iff, le_iff_le_of_cmp_eq_cmp h,
    le_iff_le_of_cmp_eq_cmp (cmp_eq_cmp_symm.1 h)]