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

Proof state:
case P24.intro.intro.refine_2.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
⊢ (∀ (i : y.LeftMoves), P3 x₁ x₂ (y.moveLeft i) y) ∧ ∀ (j : (-y).LeftMoves), P3 x₁ x₂ ((-y).moveLeft j) (-y)

Tactic:
obtain ⟨⟨h₁, -⟩, h₂, -⟩ := mulOptionsLTMul_of_numeric hn₂

Result:
case P24.intro.intro.refine_2.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)
⊢ (∀ (i : y.LeftMoves), P3 x₁ x₂ (y.moveLeft i) y) ∧ ∀ (j : (-y).LeftMoves), P3 x₁ x₂ ((-y).moveLeft j) (-y)

Proof state:
case P24.intro.intro.refine_1
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)
he : x₁ ≈ x₂
⊢ x₁ * y ≈ x₂ * y

Tactic:
rw [Args.numeric_P24] at ha

Result:
case P24.intro.intro.refine_1
a : Args
x₁ x₂ y : PGame
ha : x₁.Numeric ∧ x₂.Numeric ∧ 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)
he : x₁ ≈ x₂
⊢ x₁ * y ≈ x₂ * y

Proof state:
a : Args
⊢ a.Numeric → P124 a

Tactic:
apply argsRel_wf.induction a

Result:
a : Args
⊢ ∀ (x : Args), (∀ (y : Args), ArgsRel y x → y.Numeric → P124 y) → x.Numeric → P124 x

Proof state:
case P24.intro.intro.refine_2
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₂
⊢ (∀ (i : y.LeftMoves), P3 x₁ x₂ (y.moveLeft i) y) ∧ ∀ (j : (-y).LeftMoves), P3 x₁ x₂ ((-y).moveLeft j) (-y)

Tactic:
obtain ⟨hn₁, hn₂⟩ := numeric_of_ih ih

Result:
case P24.intro.intro.refine_2.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
⊢ (∀ (i : y.LeftMoves), P3 x₁ x₂ (y.moveLeft i) y) ∧ ∀ (j : (-y).LeftMoves), P3 x₁ x₂ ((-y).moveLeft j) (-y)

Proof state:
case P1
a : Args
x y : PGame
ha : (Args.P1 x y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P1 x y) → P124 a'
⊢ P124 (Args.P1 x y)

Tactic:
rw [Args.numeric_P1] at ha

Result:
case P1
a : Args
x y : PGame
ha : x.Numeric ∧ y.Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P1 x y) → P124 a'
⊢ P124 (Args.P1 x y)