case neg
α✝ : Type ?u.181
β : Type ?u.184
α : Type u_1
inst✝² : LE α
inst✝¹ : IsTotal α 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.181
β : Type ?u.184
α : Type u_1
inst✝² : LE α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x y : α
⊢ Ordering.swap (cmpLE x y) = cmpLE y x
by_cases xy:x ≤ y <;> by_cases yx:y ≤ x <;> simp [cmpLE, *, Ordering.swap]
no goals
case neg
α✝ : Type ?u.181
β : Type ?u.184
α : Type u_1
inst✝² : LE α
inst✝¹ : IsTotal α 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 _ _ _)