case neg
α✝ : Type ?u.3620
β : Type ?u.3623
α : Type u_1
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ False
α✝ : Type ?u.3620
β : Type ?u.3623
α : Type u_1
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
⊢ cmpLE x y = cmp x y
by_cases xy:x ≤ y <;> by_cases yx:y ≤ x <;> simp [cmpLE, lt_iff_le_not_le, *, cmp, cmpUsing]
no goals
case neg
α✝ : Type ?u.3620
β : Type ?u.3623
α : Type u_1
inst✝³ : Preorder α
inst✝² : IsTotal α fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x < x_1
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ False
cases not_or_of_not xy yx (total_of _ _ _)