-- Mathlib/SetTheory/Surreal/Multiplication.lean
theorem main (a : Args) : a.Numeric → P124 a

Proof state:
case P24.intro.intro.refine_2.intro.intro.intro.intro.intro.intro.intro
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
h4 : IH4 x₁ x₂ y
h₁₂x : IH24 (-x₂) (-x₁) y
h₁₂y : IH24 x₁ x₂ (-y)
h4x : IH4 (-x₂) (-x₁) y
h4y : IH4 x₁ x₂ (-y)
hl : x₁ < x₂
hn₁ : (x₁ * y).Numeric
hn₂ : (x₂ * y).Numeric
h₁ : MulOptionsLTMul x₂ y
h₂ : MulOptionsLTMul x₂ (-y)
h₃ : MulOptionsLTMul (-x₁) (-y)
h₄ : MulOptionsLTMul (-x₁) y
⊢ (∀ (i : y.LeftMoves), P3 x₁ x₂ (y.moveLeft i) y) ∧ ∀ (j : (-y).LeftMoves), P3 x₁ x₂ ((-y).moveLeft j) (-y)

Tactic:
constructor <;> intro <;> refine P3_of_lt ?_ ?_ hl <;> intro <;> apply ih3_of_ih

Result:
case P24.intro.intro.refine_2.intro.intro.intro.intro.intro.intro.intro.left.refine_1.h24
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
h4 : IH4 x₁ x₂ y
h₁₂x : IH24 (-x₂) (-x₁) y
h₁₂y : IH24 x₁ x₂ (-y)
h4x : IH4 (-x₂) (-x₁) y
h4y : IH4 x₁ x₂ (-y)
hl : x₁ < x₂
hn₁ : (x₁ * y).Numeric
hn₂ : (x₂ * y).Numeric
h₁ : MulOptionsLTMul x₂ y
h₂ : MulOptionsLTMul x₂ (-y)
h₃ : MulOptionsLTMul (-x₁) (-y)
h₄ : MulOptionsLTMul (-x₁) y
i✝¹ : y.LeftMoves
i✝ : x₂.LeftMoves
⊢ IH24 x₁ x₂ y

case P24.intro.intro.refine_2.intro.intro.intro.intro.intro.intro.intro.left.refine_1.h4
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
h4 : IH4 x₁ x₂ y
h₁₂x : IH24 (-x₂) (-x₁) y
h₁₂y : IH24 x₁ x₂ (-y)
h4x : IH4 (-x₂) (-x₁) y
h4y : IH4 x₁ x₂ (-y)
hl : x₁ < x₂
hn₁ : (x₁ * y).Numeric
hn₂ : (x₂ * y).Numeric
h₁ : MulOptionsLTMul x₂ y
h₂ : MulOptionsLTMul x₂ (-y)
h₃ : MulOptionsLTMul (-x₁) (-y)
h₄ : MulOptionsLTMul (-x₁) y
i✝¹ : y.LeftMoves
i✝ : x₂.LeftMoves
⊢ IH4 x₁ x₂ y

case P24.intro.intro.refine_2.intro.intro.intro.intro.intro.intro.intro.left.refine_1.hl
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
h4 : IH4 x₁ x₂ y
h₁₂x : IH24 (-x₂) (-x₁) y
h₁₂y : IH24 x₁ x₂ (-y)
h4x : IH4 (-x₂) (-x₁) y
h4y : IH4 x₁ x₂ (-y)
hl : x₁ < x₂
hn₁ : (x₁ * y).Numeric
hn₂ : (x₂ * y).Numeric
h₁ : MulOptionsLTMul x₂ y
h₂ : MulOptionsLTMul x₂ (-y)
h₃ : MulOptionsLTMul (-x₁) (-y)
h₄ : MulOptionsLTMul (-x₁) y
i✝¹ : y.LeftMoves
i✝ : x₂.LeftMoves
⊢ MulOptionsLTMul x₂ y

case P24.intro.intro.refine_2.intro.intro.intro.intro.intro.intro.intro.left.refine_2.h24
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
h4 : IH4 x₁ x₂ y
h₁₂x : IH24 (-x₂) (-x₁) y
h₁₂y : IH24 x₁ x₂ (-y)
h4x : IH4 (-x₂) (-x₁) y
h4y : IH4 x₁ x₂ (-y)
hl : x₁ < x₂
hn₁ : (x₁ * y).Numeric
hn₂ : (x₂ * y).Numeric
h₁ : MulOptionsLTMul x₂ y
h₂ : MulOptionsLTMul x₂ (-y)
h₃ : MulOptionsLTMul (-x₁) (-y)
h₄ : MulOptionsLTMul (-x₁) y
i✝¹ : y.LeftMoves
i✝ : (-x₁).LeftMoves
⊢ IH24 (-x₂) (-x₁) y

case P24.intro.intro.refine_2.intro.intro.intro.intro.intro.intro.intro.left.refine_2.h4
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
h4 : IH4 x₁ x₂ y
h₁₂x : IH24 (-x₂) (-x₁) y
h₁₂y : IH24 x₁ x₂ (-y)
h4x : IH4 (-x₂) (-x₁) y
h4y : IH4 x₁ x₂ (-y)
hl : x₁ < x₂
hn₁ : (x₁ * y).Numeric
hn₂ : (x₂ * y).Numeric
h₁ : MulOptionsLTMul x₂ y
h₂ : MulOptionsLTMul x₂ (-y)
h₃ : MulOptionsLTMul (-x₁) (-y)
h₄ : MulOptionsLTMul (-x₁) y
i✝¹ : y.LeftMoves
i✝ : (-x₁).LeftMoves
⊢ IH4 (-x₂) (-x₁) y

case P24.intro.intro.refine_2.intro.intro.intro.intro.intro.intro.intro.left.refine_2.hl
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
h4 : IH4 x₁ x₂ y
h₁₂x : IH24 (-x₂) (-x₁) y
h₁₂y : IH24 x₁ x₂ (-y)
h4x : IH4 (-x₂) (-x₁) y
h4y : IH4 x₁ x₂ (-y)
hl : x₁ < x₂
hn₁ : (x₁ * y).Numeric
hn₂ : (x₂ * y).Numeric
h₁ : MulOptionsLTMul x₂ y
h₂ : MulOptionsLTMul x₂ (-y)
h₃ : MulOptionsLTMul (-x₁) (-y)
h₄ : MulOptionsLTMul (-x₁) y
i✝¹ : y.LeftMoves
i✝ : (-x₁).LeftMoves
⊢ MulOptionsLTMul (-x₁) y

case P24.intro.intro.refine_2.intro.intro.intro.intro.intro.intro.intro.right.refine_1.h24
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
h4 : IH4 x₁ x₂ y
h₁₂x : IH24 (-x₂) (-x₁) y
h₁₂y : IH24 x₁ x₂ (-y)
h4x : IH4 (-x₂) (-x₁) y
h4y : IH4 x₁ x₂ (-y)
hl : x₁ < x₂
hn₁ : (x₁ * y).Numeric
hn₂ : (x₂ * y).Numeric
h₁ : MulOptionsLTMul x₂ y
h₂ : MulOptionsLTMul x₂ (-y)
h₃ : MulOptionsLTMul (-x₁) (-y)
h₄ : MulOptionsLTMul (-x₁) y
j✝ : (-y).LeftMoves
i✝ : x₂.LeftMoves
⊢ IH24 x₁ x₂ (-y)

case P24.intro.intro.refine_2.intro.intro.intro.intro.intro.intro.intro.right.refine_1.h4
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
h4 : IH4 x₁ x₂ y
h₁₂x : IH24 (-x₂) (-x₁) y
h₁₂y : IH24 x₁ x₂ (-y)
h4x : IH4 (-x₂) (-x₁) y
h4y : IH4 x₁ x₂ (-y)
hl : x₁ < x₂
hn₁ : (x₁ * y).Numeric
hn₂ : (x₂ * y).Numeric
h₁ : MulOptionsLTMul x₂ y
h₂ : MulOptionsLTMul x₂ (-y)
h₃ : MulOptionsLTMul (-x₁) (-y)
h₄ : MulOptionsLTMul (-x₁) y
j✝ : (-y).LeftMoves
i✝ : x₂.LeftMoves
⊢ IH4 x₁ x₂ (-y)

case P24.intro.intro.refine_2.intro.intro.intro.intro.intro.intro.intro.right.refine_1.hl
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
h4 : IH4 x₁ x₂ y
h₁₂x : IH24 (-x₂) (-x₁) y
h₁₂y : IH24 x₁ x₂ (-y)
h4x : IH4 (-x₂) (-x₁) y
h4y : IH4 x₁ x₂ (-y)
hl : x₁ < x₂
hn₁ : (x₁ * y).Numeric
hn₂ : (x₂ * y).Numeric
h₁ : MulOptionsLTMul x₂ y
h₂ : MulOptionsLTMul x₂ (-y)
h₃ : MulOptionsLTMul (-x₁) (-y)
h₄ : MulOptionsLTMul (-x₁) y
j✝ : (-y).LeftMoves
i✝ : x₂.LeftMoves
⊢ MulOptionsLTMul x₂ (-y)

case P24.intro.intro.refine_2.intro.intro.intro.intro.intro.intro.intro.right.refine_2.h24
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
h4 : IH4 x₁ x₂ y
h₁₂x : IH24 (-x₂) (-x₁) y
h₁₂y : IH24 x₁ x₂ (-y)
h4x : IH4 (-x₂) (-x₁) y
h4y : IH4 x₁ x₂ (-y)
hl : x₁ < x₂
hn₁ : (x₁ * y).Numeric
hn₂ : (x₂ * y).Numeric
h₁ : MulOptionsLTMul x₂ y
h₂ : MulOptionsLTMul x₂ (-y)
h₃ : MulOptionsLTMul (-x₁) (-y)
h₄ : MulOptionsLTMul (-x₁) y
j✝ : (-y).LeftMoves
i✝ : (-x₁).LeftMoves
⊢ IH24 (-x₂) (-x₁) (-y)

case P24.intro.intro.refine_2.intro.intro.intro.intro.intro.intro.intro.right.refine_2.h4
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
h4 : IH4 x₁ x₂ y
h₁₂x : IH24 (-x₂) (-x₁) y
h₁₂y : IH24 x₁ x₂ (-y)
h4x : IH4 (-x₂) (-x₁) y
h4y : IH4 x₁ x₂ (-y)
hl : x₁ < x₂
hn₁ : (x₁ * y).Numeric
hn₂ : (x₂ * y).Numeric
h₁ : MulOptionsLTMul x₂ y
h₂ : MulOptionsLTMul x₂ (-y)
h₃ : MulOptionsLTMul (-x₁) (-y)
h₄ : MulOptionsLTMul (-x₁) y
j✝ : (-y).LeftMoves
i✝ : (-x₁).LeftMoves
⊢ IH4 (-x₂) (-x₁) (-y)

case P24.intro.intro.refine_2.intro.intro.intro.intro.intro.intro.intro.right.refine_2.hl
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
h4 : IH4 x₁ x₂ y
h₁₂x : IH24 (-x₂) (-x₁) y
h₁₂y : IH24 x₁ x₂ (-y)
h4x : IH4 (-x₂) (-x₁) y
h4y : IH4 x₁ x₂ (-y)
hl : x₁ < x₂
hn₁ : (x₁ * y).Numeric
hn₂ : (x₂ * y).Numeric
h₁ : MulOptionsLTMul x₂ y
h₂ : MulOptionsLTMul x₂ (-y)
h₃ : MulOptionsLTMul (-x₁) (-y)
h₄ : MulOptionsLTMul (-x₁) y
j✝ : (-y).LeftMoves
i✝ : (-x₁).LeftMoves
⊢ MulOptionsLTMul (-x₁) (-y)