-- Mathlib/SetTheory/Surreal/Multiplication.lean
/-- 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. -/
lemma mulOptionsLTMul_of_numeric (hn : (x * y).Numeric) :
    (MulOptionsLTMul x y ∧ MulOptionsLTMul (-x) (-y)) ∧
    (MulOptionsLTMul x (-y) ∧ MulOptionsLTMul (-x) y)

Proof state:
case right.refine_2
x y : PGame
hn : (x * y).Numeric
h :
  (∀ (i : x.LeftMoves) (j : (-y).LeftMoves), ⟦x * y⟧ < -⟦x.mulOption (-y) i j⟧) ∧
    ∀ (i : (-x).LeftMoves) (j : y.LeftMoves), ⟦x * y⟧ < -⟦(-x).mulOption y i j⟧
a : (-x).LeftMoves
b : y.LeftMoves
⊢ ⟦(-x).mulOption y a b⟧ < -⟦x * y⟧ → ⟦(-x).mulOption y a b⟧ < ⟦-x * y⟧

Tactic:
rw [quot_neg_mul]

Result:
case right.refine_2
x y : PGame
hn : (x * y).Numeric
h :
  (∀ (i : x.LeftMoves) (j : (-y).LeftMoves), ⟦x * y⟧ < -⟦x.mulOption (-y) i j⟧) ∧
    ∀ (i : (-x).LeftMoves) (j : y.LeftMoves), ⟦x * y⟧ < -⟦(-x).mulOption y i j⟧
a : (-x).LeftMoves
b : y.LeftMoves
⊢ ⟦(-x).mulOption y a b⟧ < -⟦x * y⟧ → ⟦(-x).mulOption y a b⟧ < -⟦x * y⟧

Proof state:
case right
x y : PGame
hn : (x * y).Numeric
h :
  (∀ (i : x.LeftMoves) (j : (-y).LeftMoves), ⟦x * y⟧ < -⟦x.mulOption (-y) i j⟧) ∧
    ∀ (i : (-x).LeftMoves) (j : y.LeftMoves), ⟦x * y⟧ < -⟦(-x).mulOption y i j⟧
⊢ MulOptionsLTMul x (-y) ∧ MulOptionsLTMul (-x) y

Tactic:
refine h.imp ?_ ?_ <;> refine forall₂_imp fun a b ↦ ?_

Result:
case right.refine_1
x y : PGame
hn : (x * y).Numeric
h :
  (∀ (i : x.LeftMoves) (j : (-y).LeftMoves), ⟦x * y⟧ < -⟦x.mulOption (-y) i j⟧) ∧
    ∀ (i : (-x).LeftMoves) (j : y.LeftMoves), ⟦x * y⟧ < -⟦(-x).mulOption y i j⟧
a : x.LeftMoves
b : (-y).LeftMoves
⊢ ⟦x * y⟧ < -⟦x.mulOption (-y) a b⟧ → ⟦x.mulOption (-y) a b⟧ < ⟦x * -y⟧

case right.refine_2
x y : PGame
hn : (x * y).Numeric
h :
  (∀ (i : x.LeftMoves) (j : (-y).LeftMoves), ⟦x * y⟧ < -⟦x.mulOption (-y) i j⟧) ∧
    ∀ (i : (-x).LeftMoves) (j : y.LeftMoves), ⟦x * y⟧ < -⟦(-x).mulOption y i j⟧
a : (-x).LeftMoves
b : y.LeftMoves
⊢ ⟦x * y⟧ < -⟦(-x).mulOption y a b⟧ → ⟦(-x).mulOption y a b⟧ < ⟦-x * y⟧

Proof state:
case h.e'_2.a
x y : PGame
hn : (x * y).Numeric
h : ∀ (i : (x * y).LeftMoves), ⟦(x * y).moveLeft i⟧ < ⟦x * y⟧
⊢ MulOptionsLTMul (-x) (-y) ↔ ∀ (i : (-x).LeftMoves) (j : (-y).LeftMoves), ⟦-x * -y⟧ > ⟦(-x).mulOption (-y) i j⟧

Tactic:
rfl

Result:
no goals

Proof state:
case right.refine_1
x y : PGame
hn : (x * y).Numeric
h :
  (∀ (i : x.LeftMoves) (j : (-y).LeftMoves), ⟦x * y⟧ < -⟦x.mulOption (-y) i j⟧) ∧
    ∀ (i : (-x).LeftMoves) (j : y.LeftMoves), ⟦x * y⟧ < -⟦(-x).mulOption y i j⟧
a : x.LeftMoves
b : (-y).LeftMoves
⊢ ⟦x.mulOption (-y) a b⟧ < -⟦x * y⟧ → ⟦x.mulOption (-y) a b⟧ < ⟦x * -y⟧

Tactic:
rw [quot_mul_neg]

Result:
case right.refine_1
x y : PGame
hn : (x * y).Numeric
h :
  (∀ (i : x.LeftMoves) (j : (-y).LeftMoves), ⟦x * y⟧ < -⟦x.mulOption (-y) i j⟧) ∧
    ∀ (i : (-x).LeftMoves) (j : y.LeftMoves), ⟦x * y⟧ < -⟦(-x).mulOption y i j⟧
a : x.LeftMoves
b : (-y).LeftMoves
⊢ ⟦x.mulOption (-y) a b⟧ < -⟦x * y⟧ → ⟦x.mulOption (-y) a b⟧ < -⟦x * y⟧

Proof state:
case right.refine_2
x y : PGame
hn : (x * y).Numeric
h :
  (∀ (i : x.LeftMoves) (j : (-y).LeftMoves), ⟦x * y⟧ < -⟦x.mulOption (-y) i j⟧) ∧
    ∀ (i : (-x).LeftMoves) (j : y.LeftMoves), ⟦x * y⟧ < -⟦(-x).mulOption y i j⟧
a : (-x).LeftMoves
b : y.LeftMoves
⊢ ⟦(-x).mulOption y a b⟧ < -⟦x * y⟧ → ⟦(-x).mulOption y a b⟧ < -⟦x * y⟧

Tactic:
exact id

Result:
no goals

Proof state:
case left
x y : PGame
hn : (x * y).Numeric
h : ∀ (i : (x * y).LeftMoves), (x * y).moveLeft i < x * y
⊢ MulOptionsLTMul x y ∧ MulOptionsLTMul (-x) (-y)

Tactic:
simp_rw [lt_iff_game_lt] at h

Result:
case left
x y : PGame
hn : (x * y).Numeric
h : ∀ (i : (x * y).LeftMoves), ⟦(x * y).moveLeft i⟧ < ⟦x * y⟧
⊢ MulOptionsLTMul x y ∧ MulOptionsLTMul (-x) (-y)

Proof state:
case left
x y : PGame
hn : (x * y).Numeric
⊢ MulOptionsLTMul x y ∧ MulOptionsLTMul (-x) (-y)

Tactic:
have h := hn.moveLeft_lt

Result:
case left
x y : PGame
hn : (x * y).Numeric
h : ∀ (i : (x * y).LeftMoves), (x * y).moveLeft i < x * y
⊢ MulOptionsLTMul x y ∧ MulOptionsLTMul (-x) (-y)

Proof state:
case right
x y : PGame
hn : (x * y).Numeric
⊢ MulOptionsLTMul x (-y) ∧ MulOptionsLTMul (-x) y

Tactic:
have h := hn.lt_moveRight

Result:
case right
x y : PGame
hn : (x * y).Numeric
h : ∀ (j : (x * y).RightMoves), x * y < (x * y).moveRight j
⊢ MulOptionsLTMul x (-y) ∧ MulOptionsLTMul (-x) y

Proof state:
case right.refine_2
x y : PGame
hn : (x * y).Numeric
h :
  (∀ (i : x.LeftMoves) (j : (-y).LeftMoves), ⟦x * y⟧ < -⟦x.mulOption (-y) i j⟧) ∧
    ∀ (i : (-x).LeftMoves) (j : y.LeftMoves), ⟦x * y⟧ < -⟦(-x).mulOption y i j⟧
a : (-x).LeftMoves
b : y.LeftMoves
⊢ ⟦(-x).mulOption y a b⟧ < -⟦x * y⟧ → ⟦(-x).mulOption y a b⟧ < ⟦-x * y⟧

Tactic:
first | rw [quot_mul_neg] | rw [quot_neg_mul]

Result:
case right.refine_2
x y : PGame
hn : (x * y).Numeric
h :
  (∀ (i : x.LeftMoves) (j : (-y).LeftMoves), ⟦x * y⟧ < -⟦x.mulOption (-y) i j⟧) ∧
    ∀ (i : (-x).LeftMoves) (j : y.LeftMoves), ⟦x * y⟧ < -⟦(-x).mulOption y i j⟧
a : (-x).LeftMoves
b : y.LeftMoves
⊢ ⟦(-x).mulOption y a b⟧ < -⟦x * y⟧ → ⟦(-x).mulOption y a b⟧ < -⟦x * y⟧

Proof state:
x y : PGame
hn : (x * y).Numeric
⊢ (MulOptionsLTMul x y ∧ MulOptionsLTMul (-x) (-y)) ∧ MulOptionsLTMul x (-y) ∧ MulOptionsLTMul (-x) y

Tactic:
constructor

Result:
case left
x y : PGame
hn : (x * y).Numeric
⊢ MulOptionsLTMul x y ∧ MulOptionsLTMul (-x) (-y)

case right
x y : PGame
hn : (x * y).Numeric
⊢ MulOptionsLTMul x (-y) ∧ MulOptionsLTMul (-x) y

Proof state:
case right.refine_1
x y : PGame
hn : (x * y).Numeric
h :
  (∀ (i : x.LeftMoves) (j : (-y).LeftMoves), ⟦x * y⟧ < -⟦x.mulOption (-y) i j⟧) ∧
    ∀ (i : (-x).LeftMoves) (j : y.LeftMoves), ⟦x * y⟧ < -⟦(-x).mulOption y i j⟧
a : x.LeftMoves
b : (-y).LeftMoves
⊢ ⟦x * y⟧ < -⟦x.mulOption (-y) a b⟧ → ⟦x.mulOption (-y) a b⟧ < ⟦x * -y⟧

case right.refine_2
x y : PGame
hn : (x * y).Numeric
h :
  (∀ (i : x.LeftMoves) (j : (-y).LeftMoves), ⟦x * y⟧ < -⟦x.mulOption (-y) i j⟧) ∧
    ∀ (i : (-x).LeftMoves) (j : y.LeftMoves), ⟦x * y⟧ < -⟦(-x).mulOption y i j⟧
a : (-x).LeftMoves
b : y.LeftMoves
⊢ ⟦x * y⟧ < -⟦(-x).mulOption y a b⟧ → ⟦(-x).mulOption y a b⟧ < ⟦-x * y⟧

Tactic:
all_goals
  rw [lt_neg]
  first | rw [quot_mul_neg] | rw [quot_neg_mul]
  exact id

Result:
no goals

Proof state:
case h.e'_2.a
x y : PGame
hn : (x * y).Numeric
h : ∀ (i : (x * y).LeftMoves), ⟦(x * y).moveLeft i⟧ < ⟦x * y⟧
⊢ MulOptionsLTMul (-x) (-y) ↔ ∀ (i : (-x).LeftMoves) (j : (-y).LeftMoves), ⟦x * y⟧ > ⟦(-x).mulOption (-y) i j⟧

Tactic:
rw [← quot_neg_mul_neg]

Result:
case h.e'_2.a
x y : PGame
hn : (x * y).Numeric
h : ∀ (i : (x * y).LeftMoves), ⟦(x * y).moveLeft i⟧ < ⟦x * y⟧
⊢ MulOptionsLTMul (-x) (-y) ↔ ∀ (i : (-x).LeftMoves) (j : (-y).LeftMoves), ⟦-x * -y⟧ > ⟦(-x).mulOption (-y) i j⟧

Proof state:
case right
x y : PGame
hn : (x * y).Numeric
h : ∀ (j : (x * y).RightMoves), x * y < (x * y).moveRight j
⊢ MulOptionsLTMul x (-y) ∧ MulOptionsLTMul (-x) y

Tactic:
simp_rw [lt_iff_game_lt, rightMoves_mul_iff] at h

Result:
case right
x y : PGame
hn : (x * y).Numeric
h :
  (∀ (i : x.LeftMoves) (j : (-y).LeftMoves), ⟦x * y⟧ < -⟦x.mulOption (-y) i j⟧) ∧
    ∀ (i : (-x).LeftMoves) (j : y.LeftMoves), ⟦x * y⟧ < -⟦(-x).mulOption y i j⟧
⊢ MulOptionsLTMul x (-y) ∧ MulOptionsLTMul (-x) y