unfold compareOfLE
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
⊢ compareOfLE x y = eq → x = y
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt) = eq → x = y