-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma mulOption_lt (hx : x.Numeric) (hy : y.Numeric) (ihxy : IH1 x y) (ihyx : IH1 y x) (i j k l) :
    (⟦mulOption x y i k⟧ : Game) < -⟦mulOption x (-y) j l⟧

Proof state:
case inr.inr
x y : PGame
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
i j : x.LeftMoves
k : y.LeftMoves
l : (-y).LeftMoves
h : x.moveLeft j < x.moveLeft i
⊢ ⟦x.mulOption (-y) j l⟧ < -⟦x.mulOption (- -y) i (toLeftMovesNeg (toRightMovesNeg k))⟧

Tactic:
exact mulOption_lt_of_lt hy.neg (ih1_neg_right ihxy) (ih1_neg_left ihyx) j i l _ h

Result:
no goals

Proof state:
case inr.inl
x y : PGame
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
i j : x.LeftMoves
k : y.LeftMoves
l : (-y).LeftMoves
h : x.moveLeft i ≈ x.moveLeft j
⊢ ⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧

Tactic:
have ml := @IsOption.moveLeft

Result:
case inr.inl
x y : PGame
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
i j : x.LeftMoves
k : y.LeftMoves
l : (-y).LeftMoves
h : x.moveLeft i ≈ x.moveLeft j
ml : ∀ {x : PGame} (i : x.LeftMoves), (x.moveLeft i).IsOption x
⊢ ⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧

Proof state:
case inr.inr
x y : PGame
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
i j : x.LeftMoves
k : y.LeftMoves
l : (-y).LeftMoves
h : x.moveLeft j < x.moveLeft i
⊢ ⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧

Tactic:
rw [mulOption_neg_neg, lt_neg]

Result:
case inr.inr
x y : PGame
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
i j : x.LeftMoves
k : y.LeftMoves
l : (-y).LeftMoves
h : x.moveLeft j < x.moveLeft i
⊢ ⟦x.mulOption (-y) j l⟧ < -⟦x.mulOption (- -y) i (toLeftMovesNeg (toRightMovesNeg k))⟧

Proof state:
x y : PGame
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
i j : x.LeftMoves
k : y.LeftMoves
l : (-y).LeftMoves
⊢ ⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧

Tactic:
obtain (h|h|h) := lt_or_equiv_or_gt (hx.moveLeft i) (hx.moveLeft j)

Result:
case inl
x y : PGame
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
i j : x.LeftMoves
k : y.LeftMoves
l : (-y).LeftMoves
h : x.moveLeft i < x.moveLeft j
⊢ ⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧

case inr.inl
x y : PGame
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
i j : x.LeftMoves
k : y.LeftMoves
l : (-y).LeftMoves
h : x.moveLeft i ≈ x.moveLeft j
⊢ ⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧

case inr.inr
x y : PGame
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
i j : x.LeftMoves
k : y.LeftMoves
l : (-y).LeftMoves
h : x.moveLeft j < x.moveLeft i
⊢ ⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧

Proof state:
case inl
x y : PGame
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
i j : x.LeftMoves
k : y.LeftMoves
l : (-y).LeftMoves
h : x.moveLeft i < x.moveLeft j
⊢ ⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧

Tactic:
exact mulOption_lt_of_lt hy ihxy ihyx i j k l h

Result:
no goals

Proof state:
case inr.inl
x y : PGame
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
i j : x.LeftMoves
k : y.LeftMoves
l : (-y).LeftMoves
h : x.moveLeft i ≈ x.moveLeft j
ml : ∀ {x : PGame} (i : x.LeftMoves), (x.moveLeft i).IsOption x
⊢ ⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧

Tactic:
exact mulOption_lt_iff_P1.2 (P1_of_eq h (P24_of_ih ihxy i j).1
  (ihxy (ml i) (ml j) <| Or.inr <| isOption_neg.1 <| ml l).1 <| P3_of_ih hy ihyx i k l)

Result:
no goals