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

Proof state:
case P24
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
⊢ P124 (Args.P24 x₁ x₂ y)

Tactic:
have h₂₁ := ih₂₁ ih

Result:
case P24
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
⊢ P124 (Args.P24 x₁ x₂ y)

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

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

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

Proof state:
case P24.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)
⊢ P124 (Args.P24 x₁ x₂ y)

Tactic:
refine ⟨fun he ↦ Quotient.sound ?_, fun hl ↦ ?_⟩

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

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)

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

Tactic:
exact P1_of_ih ih ha.1 ha.2

Result:
no goals

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

Tactic:
exact ⟨mul_right_le_of_equiv ha.1 ha.2.1 h₁₂ h₂₁ he,
  mul_right_le_of_equiv ha.2.1 ha.1 h₂₁ h₁₂ (symm he)⟩

Result:
no goals

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

Tactic:
assumption

Result:
no goals

Proof state:
a✝ a : Args
ih : ∀ (y : Args), ArgsRel y a → y.Numeric → P124 y
ha : a.Numeric
⊢ P124 a

Tactic:
replace ih : ∀ a', ArgsRel a' a → P124 a' := fun a' hr ↦ ih a' hr (hr.numeric_closed ha)

Result:
a✝ a : Args
ha : a.Numeric
ih : ∀ (a' : Args), ArgsRel a' a → P124 a'
⊢ P124 a

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

Tactic:
exacts [(ih24_neg h₁₂y).1, (ih4_neg h4y).1]

Result:
no goals

Proof state:
case P24
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
⊢ P124 (Args.P24 x₁ x₂ y)

Tactic:
have h4 := ih4 ih

Result:
case P24
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
⊢ P124 (Args.P24 x₁ x₂ y)