-- Mathlib/SetTheory/Surreal/Multiplication.lean
theorem P3_of_lt_of_lt (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hy₁ : y₁.Numeric) (hy₂ : y₂.Numeric)
    (hx : x₁ < x₂) (hy : y₁ < y₂) : P3 x₁ x₂ y₁ y₂

Proof state:
case mk
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
x₁ x₂ : PGame
ih :
  ∀ (y : PGame × PGame),
    Prod.GameAdd IsOption IsOption y (x₁, x₂) → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂
hx₁ : (x₁, x₂).1.Numeric
hx₂ : (x₁, x₂).2.Numeric
hx : (x₁, x₂).1 < (x₁, x₂).2
⊢ P3 (x₁, x₂).1 (x₁, x₂).2 y₁ y₂

Tactic:
refine P3_of_lt ?_ ?_ hx <;> intro i

Result:
case mk.refine_1
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
x₁ x₂ : PGame
ih :
  ∀ (y : PGame × PGame),
    Prod.GameAdd IsOption IsOption y (x₁, x₂) → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂
hx₁ : (x₁, x₂).1.Numeric
hx₂ : (x₁, x₂).2.Numeric
hx : (x₁, x₂).1 < (x₁, x₂).2
i : (x₁, x₂).2.LeftMoves
⊢ IH3 (x₁, x₂).1 ((x₁, x₂).2.moveLeft i) (x₁, x₂).2 y₁ y₂

case mk.refine_2
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
x₁ x₂ : PGame
ih :
  ∀ (y : PGame × PGame),
    Prod.GameAdd IsOption IsOption y (x₁, x₂) → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂
hx₁ : (x₁, x₂).1.Numeric
hx₂ : (x₁, x₂).2.Numeric
hx : (x₁, x₂).1 < (x₁, x₂).2
i : (-(x₁, x₂).1).LeftMoves
⊢ IH3 (-(x₁, x₂).2) ((-(x₁, x₂).1).moveLeft i) (-(x₁, x₂).1) y₁ y₂

Proof state:
case mk.refine_1
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
x₁ x₂ : PGame
ih :
  ∀ (y : PGame × PGame),
    Prod.GameAdd IsOption IsOption y (x₁, x₂) → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂
hx₁ : (x₁, x₂).1.Numeric
hx₂ : (x₁, x₂).2.Numeric
hx : (x₁, x₂).1 < (x₁, x₂).2
i : (x₁, x₂).2.LeftMoves
⊢ IH3 (x₁, x₂).1 ((x₁, x₂).2.moveLeft i) (x₁, x₂).2 y₁ y₂

Tactic:
have hi := hx₂.moveLeft i

Result:
case mk.refine_1
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
x₁ x₂ : PGame
ih :
  ∀ (y : PGame × PGame),
    Prod.GameAdd IsOption IsOption y (x₁, x₂) → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂
hx₁ : (x₁, x₂).1.Numeric
hx₂ : (x₁, x₂).2.Numeric
hx : (x₁, x₂).1 < (x₁, x₂).2
i : (x₁, x₂).2.LeftMoves
hi : ((x₁, x₂).2.moveLeft i).Numeric
⊢ IH3 (x₁, x₂).1 ((x₁, x₂).2.moveLeft i) (x₁, x₂).2 y₁ y₂

Proof state:
x₁ x₂ y₁ y₂ : PGame
hx₁ : x₁.Numeric
hx₂ : x₂.Numeric
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hx : x₁ < x₂
hy : y₁ < y₂
⊢ P3 x₁ x₂ y₁ y₂

Tactic:
revert x₁ x₂

Result:
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
⊢ ∀ {x₁ x₂ : PGame}, x₁.Numeric → x₂.Numeric → x₁ < x₂ → P3 x₁ x₂ y₁ y₂

Proof state:
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
x₁ x₂ : PGame
ih :
  ∀ (y : PGame × PGame),
    Prod.GameAdd IsOption IsOption y (x₁, x₂) → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂
hx₁ : (x₁, x₂).1.Numeric
hx₂ : (x₁, x₂).2.Numeric
hx : (x₁, x₂).1 < (x₁, x₂).2
i : (-(x₁, x₂).1).LeftMoves
hi : ((-(x₁, x₂).1).moveLeft i).Numeric
⊢ -(x₁, x₂).2 < (-(x₁, x₂).1).moveLeft i → P3 (-(x₁, x₂).2) ((-(x₁, x₂).1).moveLeft i) y₁ y₂

Tactic:
rw [moveLeft_neg, ← P3_neg, neg_lt_neg_iff]

Result:
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
x₁ x₂ : PGame
ih :
  ∀ (y : PGame × PGame),
    Prod.GameAdd IsOption IsOption y (x₁, x₂) → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂
hx₁ : (x₁, x₂).1.Numeric
hx₂ : (x₁, x₂).2.Numeric
hx : (x₁, x₂).1 < (x₁, x₂).2
i : (-(x₁, x₂).1).LeftMoves
hi : ((-(x₁, x₂).1).moveLeft i).Numeric
⊢ (x₁, x₂).1.moveRight (toLeftMovesNeg.symm i) < (x₁, x₂).2 →
    P3 ((x₁, x₂).1.moveRight (toLeftMovesNeg.symm i)) (x₁, x₂).2 y₁ y₂

Proof state:
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
⊢ ∀ {x₁ x₂ : PGame}, x₁.Numeric → x₂.Numeric → x₁ < x₂ → P3 x₁ x₂ y₁ y₂

Tactic:
rw [← Prod.forall']

Result:
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
⊢ ∀ (x : PGame × PGame), x.1.Numeric → x.2.Numeric → x.1 < x.2 → P3 x.1 x.2 y₁ y₂

Proof state:
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
x₁ x₂ : PGame
ih :
  ∀ (y : PGame × PGame),
    Prod.GameAdd IsOption IsOption y (x₁, x₂) → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂
hx₁ : (x₁, x₂).1.Numeric
hx₂ : (x₁, x₂).2.Numeric
hx : (x₁, x₂).1 < (x₁, x₂).2
i : (-(x₁, x₂).1).LeftMoves
hi : ((-(x₁, x₂).1).moveLeft i).Numeric
⊢ (x₁, x₂).1.moveRight (toLeftMovesNeg.symm i) < (x₁, x₂).2 →
    P3 ((x₁, x₂).1.moveRight (toLeftMovesNeg.symm i)) (x₁, x₂).2 y₁ y₂

Tactic:
exact ih _ (fst <| IsOption.moveRight _) (hx₁.moveRight _) hx₂

Result:
no goals

Proof state:
case mk.refine_2
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
x₁ x₂ : PGame
ih :
  ∀ (y : PGame × PGame),
    Prod.GameAdd IsOption IsOption y (x₁, x₂) → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂
hx₁ : (x₁, x₂).1.Numeric
hx₂ : (x₁, x₂).2.Numeric
hx : (x₁, x₂).1 < (x₁, x₂).2
i : (-(x₁, x₂).1).LeftMoves
⊢ IH3 (-(x₁, x₂).2) ((-(x₁, x₂).1).moveLeft i) (-(x₁, x₂).1) y₁ y₂

Tactic:
have hi := hx₁.neg.moveLeft i

Result:
case mk.refine_2
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
x₁ x₂ : PGame
ih :
  ∀ (y : PGame × PGame),
    Prod.GameAdd IsOption IsOption y (x₁, x₂) → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂
hx₁ : (x₁, x₂).1.Numeric
hx₂ : (x₁, x₂).2.Numeric
hx : (x₁, x₂).1 < (x₁, x₂).2
i : (-(x₁, x₂).1).LeftMoves
hi : ((-(x₁, x₂).1).moveLeft i).Numeric
⊢ IH3 (-(x₁, x₂).2) ((-(x₁, x₂).1).moveLeft i) (-(x₁, x₂).1) y₁ y₂

Proof state:
case mk.refine_2
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
x₁ x₂ : PGame
ih :
  ∀ (y : PGame × PGame),
    Prod.GameAdd IsOption IsOption y (x₁, x₂) → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂
hx₁ : (x₁, x₂).1.Numeric
hx₂ : (x₁, x₂).2.Numeric
hx : (x₁, x₂).1 < (x₁, x₂).2
i : (-(x₁, x₂).1).LeftMoves
hi : ((-(x₁, x₂).1).moveLeft i).Numeric
⊢ IH3 (-(x₁, x₂).2) ((-(x₁, x₂).1).moveLeft i) (-(x₁, x₂).1) y₁ y₂

Tactic:
exact ⟨(P24 hx₂.neg hi hy₁).1, (P24 hx₂.neg hi hy₂).1,
  P3_comm.2 <| ((P24 hy₁ hy₂ hx₁).2 hy).2 _, by
    rw [moveLeft_neg, ← P3_neg, neg_lt_neg_iff]
    exact ih _ (fst <| IsOption.moveRight _) (hx₁.moveRight _) hx₂⟩

Result:
no goals

Proof state:
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
⊢ ∀ (x : PGame × PGame), x.1.Numeric → x.2.Numeric → x.1 < x.2 → P3 x.1 x.2 y₁ y₂

Tactic:
refine (wf_isOption.prod_gameAdd wf_isOption).fix ?_

Result:
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
⊢ ∀ (x : PGame × PGame),
    (∀ (y : PGame × PGame),
        Prod.GameAdd IsOption IsOption y x → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂) →
      x.1.Numeric → x.2.Numeric → x.1 < x.2 → P3 x.1 x.2 y₁ y₂

Proof state:
case mk.refine_1
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
x₁ x₂ : PGame
ih :
  ∀ (y : PGame × PGame),
    Prod.GameAdd IsOption IsOption y (x₁, x₂) → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂
hx₁ : (x₁, x₂).1.Numeric
hx₂ : (x₁, x₂).2.Numeric
hx : (x₁, x₂).1 < (x₁, x₂).2
i : (x₁, x₂).2.LeftMoves
hi : ((x₁, x₂).2.moveLeft i).Numeric
⊢ IH3 (x₁, x₂).1 ((x₁, x₂).2.moveLeft i) (x₁, x₂).2 y₁ y₂

Tactic:
exact ⟨(P24 hx₁ hi hy₁).1, (P24 hx₁ hi hy₂).1,
  P3_comm.2 <| ((P24 hy₁ hy₂ hx₂).2 hy).1 _,
  ih _ (snd <| IsOption.moveLeft i) hx₁ hi⟩

Result:
no goals

Proof state:
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
⊢ ∀ (x : PGame × PGame),
    (∀ (y : PGame × PGame),
        Prod.GameAdd IsOption IsOption y x → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂) →
      x.1.Numeric → x.2.Numeric → x.1 < x.2 → P3 x.1 x.2 y₁ y₂

Tactic:
rintro ⟨x₁, x₂⟩ ih hx₁ hx₂ hx

Result:
case mk
y₁ y₂ : PGame
hy₁ : y₁.Numeric
hy₂ : y₂.Numeric
hy : y₁ < y₂
x₁ x₂ : PGame
ih :
  ∀ (y : PGame × PGame),
    Prod.GameAdd IsOption IsOption y (x₁, x₂) → y.1.Numeric → y.2.Numeric → y.1 < y.2 → P3 y.1 y.2 y₁ y₂
hx₁ : (x₁, x₂).1.Numeric
hx₂ : (x₁, x₂).2.Numeric
hx : (x₁, x₂).1 < (x₁, x₂).2
⊢ P3 (x₁, x₂).1 (x₁, x₂).2 y₁ y₂