-- 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_3.mk
y : PGame
hy : y.Numeric
α✝ β✝ : Type u
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 (PGame.mk α✝ β✝ a✝¹ a✝) y) → P124 a
hx : (PGame.mk α✝ β✝ a✝¹ a✝).Numeric
ihxy : IH1 (PGame.mk α✝ β✝ a✝¹ a✝) y
ihyx : IH1 y (PGame.mk α✝ β✝ a✝¹ a✝)
ihxyn : IH1 (-PGame.mk α✝ β✝ a✝¹ a✝) (-y)
ihyxn : IH1 (-y) (-PGame.mk α✝ β✝ a✝¹ a✝)
⊢ ∀ (j : (PGame.mk α✝ β✝ a✝¹ a✝ * y).RightMoves), ((PGame.mk α✝ β✝ a✝¹ a✝ * y).moveRight j).Numeric

Tactic:
cases y

Result:
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

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
ihyx : IH1 y x
ihxyn : IH1 (-x) (-y)
⊢ (x * y).Numeric

Tactic:
have ihyxn := ih1_neg_left (ih1_neg_right ihyx)

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
ihxyn : IH1 (-x) (-y)
ihyxn : IH1 (-y) (-x)
⊢ (x * y).Numeric

Proof state:
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⟧

Tactic:
rw [mulOption_neg_neg y]

Result:
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 (toLeftMovesNeg (toRightMovesNeg l))⟧ > ⟦(-x).mulOption (-y) i k⟧

Proof state:
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 (toLeftMovesNeg (toRightMovesNeg l))⟧ > ⟦(-x).mulOption (-y) i k⟧

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

Result:
no goals

Proof state:
case refine_3
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 * y).RightMoves), ((x * y).moveRight j).Numeric

Tactic:
cases x

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

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
ihyx : IH1 y x
⊢ (x * y).Numeric

Tactic:
have ihxyn := ih1_neg_left (ih1_neg_right ihxy)

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
ihxyn : IH1 (-x) (-y)
⊢ (x * y).Numeric

Proof state:
case refine_1.left.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⟧

Tactic:
apply mulOption_lt hx hy ihxy ihyx

Result:
no goals

Proof state:
case refine_2
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), ((x * y).moveLeft i).Numeric

case refine_3
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 * y).RightMoves), ((x * y).moveRight j).Numeric

Tactic:
all_goals
  cases x; cases y
  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:
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)
⊢ (x * y).Numeric

Tactic:
refine numeric_def.mpr ⟨?_, ?_, ?_⟩

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

case refine_2
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), ((x * y).moveLeft i).Numeric

case refine_3
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 * y).RightMoves), ((x * y).moveRight j).Numeric

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
⊢ -⟦(-x).mulOption y j l⟧ > ⟦x.mulOption y i k⟧

Tactic:
simp only [← mulOption_symm y]

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
⊢ -⟦y.mulOption (-x) l j⟧ > ⟦y.mulOption x k i⟧

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
⊢ ∀ (i_1 : (-x).LeftMoves) (j : y.LeftMoves), ⟦(x * y).moveLeft i⟧ < -⟦(-x).mulOption y i_1 j⟧

Tactic:
intro j l

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)
i : (x * y).LeftMoves
j : (-x).LeftMoves
l : y.LeftMoves
⊢ ⟦(x * y).moveLeft i⟧ < -⟦(-x).mulOption y j l⟧