α : Type u_1
β : Type ?u.12785
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
⊢ swap (if (fun x x_1 => x < x_1) a b then lt else if (fun x x_1 => x < x_1) b a then gt else eq) =
    if (fun x x_1 => x < x_1) b a then lt else if (fun x x_1 => x < x_1) a b then gt else eq
α : Type u_1
β : Type ?u.12785
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
⊢ swap (cmp a b) = cmp b a
unfold cmp cmpUsing
case pos
α : Type u_1
β : Type ?u.12785
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
h : a < b
h₂ : b < a
⊢ False
α : Type u_1
β : Type ?u.12785
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
⊢ swap (if (fun x x_1 => x < x_1) a b then lt else if (fun x x_1 => x < x_1) b a then gt else eq) =
    if (fun x x_1 => x < x_1) b a then lt else if (fun x x_1 => x < x_1) a b then gt else eq
by_cases h : a < b <;> by_cases h₂ : b < a <;> simp [h, h₂, Ordering.swap]
no goals
case pos
α : Type u_1
β : Type ?u.12785
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a b : α
h : a < b
h₂ : b < a
⊢ False
exact lt_asymm h h₂