English
If x and x' are numeric and x' ≤ x, then insertLeft(x, x') is numeric.
Русский
Если x и x' числовые и x' ≤ x, то вставка слева x' к x числовая.
LaTeX
$$$(Numeric(x) \land Numeric(x') \land x' \le x) \Rightarrow Numeric(x.insertLeft(x'))$$$
Lean4
/-- Inserting a smaller numeric left option into a numeric game results in a numeric game. -/
theorem insertLeft_numeric {x x' : PGame} (x_num : x.Numeric) (x'_num : x'.Numeric) (h : x' ≤ x) :
(insertLeft x x').Numeric := by
rw [le_iff_forall_lt x'_num x_num] at h
unfold Numeric at x_num ⊢
rcases x with ⟨xl, xr, xL, xR⟩
simp only [insertLeft, Sum.forall, forall_const, Sum.elim_inl, Sum.elim_inr] at x_num ⊢
constructor
· simp only [x_num.1, implies_true, true_and]
simp only [rightMoves_mk, moveRight_mk] at h
exact h.2
· simp only [x_num, implies_true, x'_num, and_self]
