no goals
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ GameAdd rβ rα (swap (a₁, b₁)) (swap (a₂, b₂)) ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
rw [Prod.swap, Prod.swap, gameAdd_mk_iff, gameAdd_mk_iff, or_comm]