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

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

case gt
α : Type u_1
β : Type ?u.6152
inst✝ : LT α
a b : α
⊢ Compares (swap gt) a b ↔ Compares gt b a
α : Type u_1
β : Type ?u.6152
inst✝ : LT α
a b : α
o : Ordering
⊢ Compares (swap o) a b ↔ Compares o b a
cases o
no goals
case lt
α : Type u_1
β : Type ?u.6152
inst✝ : LT α
a b : α
⊢ Compares (swap lt) a b ↔ Compares lt b a
exact Iff.rfl
no goals
case eq
α : Type u_1
β : Type ?u.6152
inst✝ : LT α
a b : α
⊢ Compares (swap eq) a b ↔ Compares eq b a
exact eq_comm
no goals
case gt
α : Type u_1
β : Type ?u.6152
inst✝ : LT α
a b : α
⊢ Compares (swap gt) a b ↔ Compares gt b a
exact Iff.rfl