next => contradiction
case isFalse
α : 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 : α
hxy : x ≤ y
h✝ : ¬y ≤ x
cxy : False
⊢ x = y
no goals