α : Type u_1
β : Type ?u.6116
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα (Quotient.mk (Rel.setoid α) (a₁, b)) (Quotient.mk (Rel.setoid α) (a₂, b))
α : Type u_1
β : Type ?u.6116
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα (Quotient.mk (Rel.setoid α) (b, a₁)) (Quotient.mk (Rel.setoid α) (a₂, b))
rw [Sym2.eq_swap]
no goals
α : Type u_1
β : Type ?u.6116
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα (Quotient.mk (Rel.setoid α) (a₁, b)) (Quotient.mk (Rel.setoid α) (a₂, b))
exact GameAdd.fst h