English
If the IH hypothesis holds for all a, then the P1 component of x*y is numeric.
Русский
Если IH выполняется для всех a, то компонент P1 x*y числовой.
LaTeX
$$$(IH \\; x y) \\\\Rightarrow (x*y).Numeric$$$
Lean4
/-- P1 follows from the induction hypothesis. -/
theorem P1_of_ih (ih : ∀ a, ArgsRel a (Args.P1 x y) → P124 a) (hx : x.Numeric) (hy : y.Numeric) : (x * y).Numeric :=
by
have ihxy := ih1 ih
have ihyx := ih1_swap ih
have ihxyn := ih1_neg_left (ih1_neg_right ihxy)
have ihyxn := ih1_neg_left (ih1_neg_right ihyx)
refine numeric_def.mpr ⟨?_, ?_, ?_⟩
· simp_rw [lt_iff_game_lt]
intro i
rw [rightMoves_mul_iff]
constructor <;> (intro j l; revert i; rw [leftMoves_mul_iff (_ > ·)]; constructor <;> intro i k)
· apply mulOption_lt hx hy ihxy ihyx
· simp_rw [← mulOption_symm (-y), mulOption_neg_neg x]
apply mulOption_lt hy.neg hx.neg ihyxn ihxyn
· simp only [← mulOption_symm y]
apply mulOption_lt hy hx ihyx ihxy
· rw [mulOption_neg_neg y]
apply mulOption_lt hx.neg hy.neg ihxyn ihyxn
all_goals
cases x; cases y
rintro (⟨i, j⟩ | ⟨i, j⟩) <;>
refine ((numeric_option_mul ih ?_).add <| numeric_mul_option ih ?_).sub (numeric_option_mul_option ih ?_ ?_) <;>
solve_by_elim [IsOption.mk_left, IsOption.mk_right]
