split at cxy
α : 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 : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) = eq
⊢ x = y
case isTrue
α : 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 : α
h✝ : x ≤ y
cxy : (if y ≤ x then eq else lt) = eq
⊢ x = y

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 : α
h✝ : ¬x ≤ y
cxy : False
⊢ x = y