English
Under numeric hx, IH24 x1 x2 y and equivalence x1 ≈ x2, for i in x1.LeftMoves and j in y.LeftMoves, mulOption x1 y i j is strictly less than the product instHMul.hMul x2 y.
Русский
При числовом hx и IH24 x1 x2 y и эквивелентности x1 ≈ x2, при i∈LeftMoves x1 и j∈LeftMoves y, mulOption x1 y i j < x2*y.
LaTeX
$$$(x_1.Numeric) \\\\wedge IH24 x_1 x_2 y \\\\wedge x_1 \\approx x_2 \\\\Rightarrow \\\\forall i\\in x_1.LeftMoves, \\forall j\\in y.LeftMoves, \\\\lt (Quotient.mk SetTheory.PGame.setoid (x_1.mulOption y i j)) (Quotient.mk SetTheory.PGame.setoid (instHMul.hMul x_2 y))$$$
Lean4
theorem mulOption_lt_mul_of_equiv (hn : x₁.Numeric) (h : IH24 x₁ x₂ y) (he : x₁ ≈ x₂) (i j) :
⟦mulOption x₁ y i j⟧ < (⟦x₂ * y⟧ : Game) :=
by
convert sub_lt_iff_lt_add'.2 ((((@h _).1 <| IsOption.moveLeft i).2 _).1 j) using 1
· rw [← ((@h _).2.2 <| IsOption.moveLeft j).1 he]
rfl
· rw [← lt_congr_right he]
apply hn.moveLeft_lt
