-- Mathlib/SetTheory/Game/Basic.lean
/-- `x * -y` and `-(x * y)` have the same moves. -/
@[simp]
lemma mul_neg (x y : PGame) : x * -y = -(x * y) :=
  match x, y with
  | mk xl xr xL xR, mk yl yr yL yR => by
    refine ext rfl rfl ?_ ?_ <;> rintro (⟨i, j⟩ | ⟨i, j⟩) _ ⟨rfl⟩
    all_goals
      dsimp
      rw [PGame.neg_sub', PGame.neg_add]
      congr
      exacts [mul_neg _ (mk ..), mul_neg .., mul_neg ..]
termination_by (x, y)

Proof state:
case refine_2.inr.mk.refl
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xr
j : yr
β : Type u_1
⊢ (xR i * mk yr yl (fun x => -yR x) fun x => -yL x) + mk xl xr xL xR * -yR j - xR i * -yR j =
    -(xR i * mk yl yr yL yR) + -(mk xl xr xL xR * yR j) - -(xR i * yR j)

Tactic:
congr

Result:
case refine_2.inr.mk.refl.e_a.e_a
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xr
j : yr
β : Type u_1
⊢ (xR i * mk yr yl (fun x => -yR x) fun x => -yL x) = -(xR i * mk yl yr yL yR)

case refine_2.inr.mk.refl.e_a.e_a
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xr
j : yr
β : Type u_1
⊢ mk xl xr xL xR * -yR j = -(mk xl xr xL xR * yR j)

case refine_2.inr.mk.refl.e_a
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xr
j : yr
β : Type u_1
⊢ xR i * -yR j = -(xR i * yR j)

Proof state:
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
⊢ mk xl xr xL xR * -mk yl yr yL yR = -(mk xl xr xL xR * mk yl yr yL yR)

Tactic:
refine ext rfl rfl ?_ ?_ <;> rintro (⟨i, j⟩ | ⟨i, j⟩) _ ⟨rfl⟩

Result:
case refine_1.inl.mk.refl
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xl
j : yr
β : Type u_1
⊢ (mk xl xr xL xR * -mk yl yr yL yR).moveLeft (Sum.inl (i, j)) =
    (-(mk xl xr xL xR * mk yl yr yL yR)).moveLeft (Sum.inl (i, j))

case refine_1.inr.mk.refl
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xr
j : yl
β : Type u_1
⊢ (mk xl xr xL xR * -mk yl yr yL yR).moveLeft (Sum.inr (i, j)) =
    (-(mk xl xr xL xR * mk yl yr yL yR)).moveLeft (Sum.inr (i, j))

case refine_2.inl.mk.refl
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xl
j : yl
β : Type u_1
⊢ (mk xl xr xL xR * -mk yl yr yL yR).moveRight (Sum.inl (i, j)) =
    (-(mk xl xr xL xR * mk yl yr yL yR)).moveRight (Sum.inl (i, j))

case refine_2.inr.mk.refl
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xr
j : yr
β : Type u_1
⊢ (mk xl xr xL xR * -mk yl yr yL yR).moveRight (Sum.inr (i, j)) =
    (-(mk xl xr xL xR * mk yl yr yL yR)).moveRight (Sum.inr (i, j))

Proof state:
case refine_2.inr.mk.refl.e_a.e_a
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xr
j : yr
β : Type u_1
⊢ (xR i * mk yr yl (fun x => -yR x) fun x => -yL x) = -(xR i * mk yl yr yL yR)

case refine_2.inr.mk.refl.e_a.e_a
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xr
j : yr
β : Type u_1
⊢ mk xl xr xL xR * -yR j = -(mk xl xr xL xR * yR j)

case refine_2.inr.mk.refl.e_a
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xr
j : yr
β : Type u_1
⊢ xR i * -yR j = -(xR i * yR j)

Tactic:
exacts [mul_neg _ (mk ..), mul_neg .., mul_neg ..]

Result:
no goals

Proof state:
case refine_2.inr.mk.refl
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xr
j : yr
β : Type u_1
⊢ (mk xl xr xL xR * -mk yl yr yL yR).moveRight (Sum.inr (i, j)) =
    (-(mk xl xr xL xR * mk yl yr yL yR)).moveRight (Sum.inr (i, j))

Tactic:
dsimp

Result:
case refine_2.inr.mk.refl
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xr
j : yr
β : Type u_1
⊢ (xR i * mk yr yl (fun x => -yR x) fun x => -yL x) + mk xl xr xL xR * -yR j - xR i * -yR j =
    -(xR i * mk yl yr yL yR + mk xl xr xL xR * yR j - xR i * yR j)

Proof state:
case refine_2.inr.mk.refl
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xr
j : yr
β : Type u_1
⊢ (xR i * mk yr yl (fun x => -yR x) fun x => -yL x) + mk xl xr xL xR * -yR j - xR i * -yR j =
    -(xR i * mk yl yr yL yR + mk xl xr xL xR * yR j - xR i * yR j)

Tactic:
rw [PGame.neg_sub', PGame.neg_add]

Result:
case refine_2.inr.mk.refl
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xr
j : yr
β : Type u_1
⊢ (xR i * mk yr yl (fun x => -yR x) fun x => -yL x) + mk xl xr xL xR * -yR j - xR i * -yR j =
    -(xR i * mk yl yr yL yR) + -(mk xl xr xL xR * yR j) - -(xR i * yR j)

Proof state:
case refine_1.inl.mk.refl
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xl
j : yr
β : Type u_1
⊢ (mk xl xr xL xR * -mk yl yr yL yR).moveLeft (Sum.inl (i, j)) =
    (-(mk xl xr xL xR * mk yl yr yL yR)).moveLeft (Sum.inl (i, j))

case refine_1.inr.mk.refl
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xr
j : yl
β : Type u_1
⊢ (mk xl xr xL xR * -mk yl yr yL yR).moveLeft (Sum.inr (i, j)) =
    (-(mk xl xr xL xR * mk yl yr yL yR)).moveLeft (Sum.inr (i, j))

case refine_2.inl.mk.refl
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xl
j : yl
β : Type u_1
⊢ (mk xl xr xL xR * -mk yl yr yL yR).moveRight (Sum.inl (i, j)) =
    (-(mk xl xr xL xR * mk yl yr yL yR)).moveRight (Sum.inl (i, j))

case refine_2.inr.mk.refl
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xr
j : yr
β : Type u_1
⊢ (mk xl xr xL xR * -mk yl yr yL yR).moveRight (Sum.inr (i, j)) =
    (-(mk xl xr xL xR * mk yl yr yL yR)).moveRight (Sum.inr (i, j))

Tactic:
all_goals
  dsimp
  rw [PGame.neg_sub', PGame.neg_add]
  congr
  exacts [mul_neg _ (mk ..), mul_neg .., mul_neg ..]

Result:
no goals