English
Let x, y be elements of α × α. Then the GameAdd relation between the Sym2 lifts of x and y holds exactly when either Prod.GameAdd holds for (x) and (y) or for (x swapped) and (y).
Русский
Пусть x, y ∈ α × α. Тогда отношение GameAdd между леммами Sym2(x) и Sym2(y) эквивалентно тому, что либо Prod.GameAdd выполняется для (x) и (y), либо для (x swapped) и (y).
LaTeX
$$$\forall x,y \in \alpha \times \alpha,\; \mathrm{GameAdd}(r_\alpha,\mathrm{Sym2.mk}(x),\mathrm{Sym2.mk}(y)) \iff \mathrm{Prod.GameAdd}(r_\alpha,r_\alpha)(x,y) \lor \mathrm{Prod.GameAdd}(r_\alpha,r_\alpha)(x^{\mathrm{swap}},y).$$$
Lean4
theorem gameAdd_iff :
∀ {x y : α × α}, GameAdd rα (Sym2.mk x) (Sym2.mk y) ↔ Prod.GameAdd rα rα x y ∨ Prod.GameAdd rα rα x.swap y :=
by
rintro ⟨_, _⟩ ⟨_, _⟩
rfl
