theorem Prod.swap_mk {α : Type u_1} {β : Type u_2} {a : α} {b : β} : (a, b).swap = (b, a)

Alias of Prod.swap_prod_mk.