English
If (x*y) is numeric, then the four MulOptionsLT terms are in a four-way conjunction capturing left and right moves for x and y and their negations.
Русский
Если (x*y) числовой, то четыре MulOptionsLT образуют связку условий, охватывающую ходы слева/справа и их отрицания.
LaTeX
$$$(x y)\\text{ Numeric} \\\\Rightarrow (MulOptionsLTMul x y) \\\\land (MulOptionsLTMul(-x)(-y)) \\\\land (MulOptionsLTMul x(-y)) \\\\land (MulOptionsLTMul(-x) y)$$$
Lean4
/-- That the left options of `x * y` are less than itself and the right options are greater, which
is part of the condition that `x * y` is numeric, is equivalent to the conjunction of various
`MulOptionsLTMul` statements for `x`, `y` and their negations. We only show the forward
direction. -/
theorem mulOptionsLTMul_of_numeric (hn : (x * y).Numeric) :
(MulOptionsLTMul x y ∧ MulOptionsLTMul (-x) (-y)) ∧ (MulOptionsLTMul x (-y) ∧ MulOptionsLTMul (-x) y) :=
by
constructor
· have h := hn.moveLeft_lt
simp_rw [lt_iff_game_lt] at h
convert (leftMoves_mul_iff <| GT.gt _).1 h
rw [← quot_neg_mul_neg]
rfl
· have h := hn.lt_moveRight
simp_rw [lt_iff_game_lt, rightMoves_mul_iff] at h
refine h.imp ?_ ?_ <;> refine forall₂_imp fun a b ↦ ?_
all_goals
rw [lt_neg]
first
| rw [quot_mul_neg]
| rw [quot_neg_mul]
exact id
