-- Mathlib/SetTheory/Surreal/Multiplication.lean
theorem P1_of_ih (ih : ∀ a, ArgsRel a (Args.P1 x y) → P124 a) (hx : x.Numeric) (hy : y.Numeric) :
    (x * y).Numeric

Proof state:
case refine_1
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
ihxyn : IH1 (-x) (-y)
ihyxn : IH1 (-y) (-x)
⊢ ∀ (i : (x * y).LeftMoves) (j : (x * y).RightMoves), ⟦(x * y).moveLeft i⟧ < ⟦(x * y).moveRight j⟧

Tactic:
intro i

Result:
case refine_1
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
ihxyn : IH1 (-x) (-y)
ihyxn : IH1 (-y) (-x)
i : (x * y).LeftMoves
⊢ ∀ (j : (x * y).RightMoves), ⟦(x * y).moveLeft i⟧ < ⟦(x * y).moveRight j⟧

Proof state:
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
⊢ (x * y).Numeric

Tactic:
have ihyx := ih1_swap ih

Result:
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
⊢ (x * y).Numeric

Proof state:
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
⊢ (x * y).Numeric

Tactic:
have ihxy := ih1 ih

Result:
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
⊢ (x * y).Numeric

Proof state:
case refine_1.left.right
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
ihxyn : IH1 (-x) (-y)
ihyxn : IH1 (-y) (-x)
j : x.LeftMoves
l : (-y).LeftMoves
i : (-x).LeftMoves
k : (-y).LeftMoves
⊢ -⟦x.mulOption (-y) j l⟧ > ⟦(-x).mulOption (-y) i k⟧

Tactic:
simp_rw [← mulOption_symm (-y), mulOption_neg_neg x]

Result:
case refine_1.left.right
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
ihxyn : IH1 (-x) (-y)
ihyxn : IH1 (-y) (-x)
j : x.LeftMoves
l : (-y).LeftMoves
i : (-x).LeftMoves
k : (-y).LeftMoves
⊢ -⟦(-y).mulOption (- -x) l (toLeftMovesNeg (toRightMovesNeg j))⟧ > ⟦(-y).mulOption (-x) k i⟧

Proof state:
case refine_1.left.right
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
ihxyn : IH1 (-x) (-y)
ihyxn : IH1 (-y) (-x)
j : x.LeftMoves
l : (-y).LeftMoves
i : (-x).LeftMoves
k : (-y).LeftMoves
⊢ -⟦(-y).mulOption (- -x) l (toLeftMovesNeg (toRightMovesNeg j))⟧ > ⟦(-y).mulOption (-x) k i⟧

Tactic:
apply mulOption_lt hy.neg hx.neg ihyxn ihxyn

Result:
no goals

Proof state:
case refine_1.right.left
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
ihxyn : IH1 (-x) (-y)
ihyxn : IH1 (-y) (-x)
j : (-x).LeftMoves
l : y.LeftMoves
i : x.LeftMoves
k : y.LeftMoves
⊢ -⟦y.mulOption (-x) l j⟧ > ⟦y.mulOption x k i⟧

Tactic:
apply mulOption_lt hy hx ihyx ihxy

Result:
no goals

Proof state:
case refine_1
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
ihxyn : IH1 (-x) (-y)
ihyxn : IH1 (-y) (-x)
i : (x * y).LeftMoves
⊢ ∀ (j : (x * y).RightMoves), ⟦(x * y).moveLeft i⟧ < ⟦(x * y).moveRight j⟧

Tactic:
rw [rightMoves_mul_iff]

Result:
case refine_1
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
ihxyn : IH1 (-x) (-y)
ihyxn : IH1 (-y) (-x)
i : (x * y).LeftMoves
⊢ (∀ (i_1 : x.LeftMoves) (j : (-y).LeftMoves), ⟦(x * y).moveLeft i⟧ < -⟦x.mulOption (-y) i_1 j⟧) ∧
    ∀ (i_1 : (-x).LeftMoves) (j : y.LeftMoves), ⟦(x * y).moveLeft i⟧ < -⟦(-x).mulOption y i_1 j⟧

Proof state:
case refine_3.mk.mk
α✝¹ β✝¹ : Type u
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
hx : (PGame.mk α✝¹ β✝¹ a✝³ a✝²).Numeric
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
hy : (PGame.mk α✝ β✝ a✝¹ a✝).Numeric
ih : ∀ (a : Args), ArgsRel a (Args.P1 (PGame.mk α✝¹ β✝¹ a✝³ a✝²) (PGame.mk α✝ β✝ a✝¹ a✝)) → P124 a
ihxy : IH1 (PGame.mk α✝¹ β✝¹ a✝³ a✝²) (PGame.mk α✝ β✝ a✝¹ a✝)
ihyx : IH1 (PGame.mk α✝ β✝ a✝¹ a✝) (PGame.mk α✝¹ β✝¹ a✝³ a✝²)
ihxyn : IH1 (-PGame.mk α✝¹ β✝¹ a✝³ a✝²) (-PGame.mk α✝ β✝ a✝¹ a✝)
ihyxn : IH1 (-PGame.mk α✝ β✝ a✝¹ a✝) (-PGame.mk α✝¹ β✝¹ a✝³ a✝²)
⊢ ∀ (j : (PGame.mk α✝¹ β✝¹ a✝³ a✝² * PGame.mk α✝ β✝ a✝¹ a✝).RightMoves),
    ((PGame.mk α✝¹ β✝¹ a✝³ a✝² * PGame.mk α✝ β✝ a✝¹ a✝).moveRight j).Numeric

Tactic:
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]

Result:
no goals

Proof state:
case refine_1
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
ihxyn : IH1 (-x) (-y)
ihyxn : IH1 (-y) (-x)
⊢ ∀ (i : (x * y).LeftMoves) (j : (x * y).RightMoves), (x * y).moveLeft i < (x * y).moveRight j

Tactic:
simp_rw [lt_iff_game_lt]

Result:
case refine_1
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
ihxyn : IH1 (-x) (-y)
ihyxn : IH1 (-y) (-x)
⊢ ∀ (i : (x * y).LeftMoves) (j : (x * y).RightMoves), ⟦(x * y).moveLeft i⟧ < ⟦(x * y).moveRight j⟧

Proof state:
case refine_1.right
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
ihxyn : IH1 (-x) (-y)
ihyxn : IH1 (-y) (-x)
i : (x * y).LeftMoves
j : (-x).LeftMoves
l : y.LeftMoves
⊢ ⟦(x * y).moveLeft i⟧ < -⟦(-x).mulOption y j l⟧

Tactic:
revert i

Result:
case refine_1.right
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
ihxyn : IH1 (-x) (-y)
ihyxn : IH1 (-y) (-x)
j : (-x).LeftMoves
l : y.LeftMoves
⊢ ∀ (i : (x * y).LeftMoves), ⟦(x * y).moveLeft i⟧ < -⟦(-x).mulOption y j l⟧

Proof state:
case refine_1.right
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
ihxyn : IH1 (-x) (-y)
ihyxn : IH1 (-y) (-x)
j : (-x).LeftMoves
l : y.LeftMoves
⊢ (∀ (i : x.LeftMoves) (j_1 : y.LeftMoves), -⟦(-x).mulOption y j l⟧ > ⟦x.mulOption y i j_1⟧) ∧
    ∀ (i : (-x).LeftMoves) (j_1 : (-y).LeftMoves), -⟦(-x).mulOption y j l⟧ > ⟦(-x).mulOption (-y) i j_1⟧

Tactic:
constructor <;> intro i k

Result:
case refine_1.right.left
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
ihxyn : IH1 (-x) (-y)
ihyxn : IH1 (-y) (-x)
j : (-x).LeftMoves
l : y.LeftMoves
i : x.LeftMoves
k : y.LeftMoves
⊢ -⟦(-x).mulOption y j l⟧ > ⟦x.mulOption y i k⟧

case refine_1.right.right
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
hx : x.Numeric
hy : y.Numeric
ihxy : IH1 x y
ihyx : IH1 y x
ihxyn : IH1 (-x) (-y)
ihyxn : IH1 (-y) (-x)
j : (-x).LeftMoves
l : y.LeftMoves
i : (-x).LeftMoves
k : (-y).LeftMoves
⊢ -⟦(-x).mulOption y j l⟧ > ⟦(-x).mulOption (-y) i k⟧