English
If x is a Right gift to x' (a Right option that does not change the value), then insertRight x x' ≈ x.
Русский
Если x является подарочным правым ходом к x' (правый ход, не меняющий стоимость), то insertRight x x' эквивалентен x.
LaTeX
$$$x \lt_{lf} x' \Rightarrow insertRight\; x\; x' \approx x$$$
Lean4
/-- Adding a gift horse right option does not change the value of `x`. A gift horse right option is
a game `x'` with `x ⧏ x'`. It is called "gift horse" because it seems like Right has gotten the
"gift" of a new option, but actually the value of the game did not change. -/
theorem insertRight_equiv_of_lf {x x' : PGame} (h : x ⧏ x') : insertRight x x' ≈ x :=
by
rw [equiv_def]
constructor
· apply insertRight_le
· rw [le_def]
constructor
· intro j
left
rcases x with ⟨xl, xr, xL, xR⟩
simp only [insertRight, moveLeft_mk]
use j
· intro i
rcases x with ⟨xl, xr, xL, xR⟩
simp only [insertRight, moveRight_mk] at i ⊢
rcases i with i | _
· rw [Sum.elim_inl]
right
use i
· rw [Sum.elim_inr]
simpa only [lf_iff_exists_le] using h
