split
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
h✝ : ¬x < y
⊢ (if y < x then gt else eq).swap = if y < x then lt else eq
case isTrue
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
h✝ : y < x
⊢ gt.swap = lt

case isFalse
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
h✝ : ¬y < x
⊢ eq.swap = eq