English
If a and b are Acc with respect to rα, then the pair (a,b) is Acc with respect to the Sym2.GameAdd relation.
Русский
Если a и b имеют Acc по отношению rα, то пара (a,b) имеет Acc по отношению Sym2.GameAdd.
LaTeX
$$$\forall a,b:\; \mathrm{Acc}\, r_\alpha(a) \rightarrow \mathrm{Acc}\, r_\alpha(b) \rightarrow \mathrm{Acc}\,(\mathrm{Sym2.GameAdd}(r_\alpha))\; (a,b).$$$
Lean4
theorem sym2_gameAdd {a b} (ha : Acc rα a) (hb : Acc rα b) : Acc (Sym2.GameAdd rα) s(a, b) :=
by
induction ha generalizing b with
| _ a _ iha
induction hb with
| _ b hb ihb
refine Acc.intro _ fun s => ?_
induction s with
| _ c d
rw [Sym2.GameAdd]
dsimp
rintro ((rc | rd) | (rd | rc))
· exact iha c rc ⟨b, hb⟩
· exact ihb d rd
· rw [Sym2.eq_swap]
exact iha d rd ⟨b, hb⟩
· rw [Sym2.eq_swap]
exact ihb c rc
