case lt
α : Type u_1
β : Type ?u.10829
inst✝ : LT α
a b : α
⊢ Compares lt (↑toDual a) (↑toDual b) ↔ Compares lt b a

case eq
α : Type u_1
β : Type ?u.10829
inst✝ : LT α
a b : α
⊢ Compares eq (↑toDual a) (↑toDual b) ↔ Compares eq b a

case gt
α : Type u_1
β : Type ?u.10829
inst✝ : LT α
a b : α
⊢ Compares gt (↑toDual a) (↑toDual b) ↔ Compares gt b a
α : Type u_1
β : Type ?u.10829
inst✝ : LT α
a b : α
o : Ordering
⊢ Compares o (↑toDual a) (↑toDual b) ↔ Compares o b a
cases o
no goals
case lt
α : Type u_1
β : Type ?u.10829
inst✝ : LT α
a b : α
⊢ Compares lt (↑toDual a) (↑toDual b) ↔ Compares lt b a

case eq
α : Type u_1
β : Type ?u.10829
inst✝ : LT α
a b : α
⊢ Compares eq (↑toDual a) (↑toDual b) ↔ Compares eq b a

case gt
α : Type u_1
β : Type ?u.10829
inst✝ : LT α
a b : α
⊢ Compares gt (↑toDual a) (↑toDual b) ↔ Compares gt b a
exacts [Iff.rfl, eq_comm, Iff.rfl]