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