case lt
α : Type u_1
β : Type ?u.11173
inst✝ : LT α
a b : αᵒᵈ
⊢ Compares lt (↑ofDual a) (↑ofDual b) ↔ Compares lt b a

case eq
α : Type u_1
β : Type ?u.11173
inst✝ : LT α
a b : αᵒᵈ
⊢ Compares eq (↑ofDual a) (↑ofDual b) ↔ Compares eq b a

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

case eq
α : Type u_1
β : Type ?u.11173
inst✝ : LT α
a b : αᵒᵈ
⊢ Compares eq (↑ofDual a) (↑ofDual b) ↔ Compares eq b a

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