-- Mathlib/SetTheory/Game/Basic.lean
/-- The left options of `x * y` of the second kind are the left options of `(-x) * (-y)` of the
  first kind, up to equivalence. -/
lemma leftMoves_mul_iff {x y : PGame} (P : Game → Prop) :
    (∀ k, P ⟦(x * y).moveLeft k⟧) ↔
    (∀ i j, P ⟦mulOption x y i j⟧) ∧ (∀ i j, P ⟦mulOption (-x) (-y) i j⟧)

Proof state:
case h.e'_1
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h :
  (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧
i : β✝¹
j : β✝
⊢ ⟦a✝² i * mk α✝ β✝ a✝¹ a✝⟧ + ⟦mk α✝¹ β✝¹ a✝³ a✝² * a✝ j⟧ - ⟦a✝² i * a✝ j⟧ =
    ⟦-a✝² i * -mk α✝ β✝ a✝¹ a✝⟧ + ⟦-mk α✝¹ β✝¹ a✝³ a✝² * -a✝ j⟧ - ⟦-a✝² i * -a✝ j⟧

Tactic:
congr 1

Result:
case h.e'_1.e_a
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h :
  (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧
i : β✝¹
j : β✝
⊢ ⟦a✝² i * mk α✝ β✝ a✝¹ a✝⟧ + ⟦mk α✝¹ β✝¹ a✝³ a✝² * a✝ j⟧ = ⟦-a✝² i * -mk α✝ β✝ a✝¹ a✝⟧ + ⟦-mk α✝¹ β✝¹ a✝³ a✝² * -a✝ j⟧

case h.e'_1.e_a
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h :
  (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧
i : β✝¹
j : β✝
⊢ ⟦a✝² i * a✝ j⟧ = ⟦-a✝² i * -a✝ j⟧

Proof state:
case h.e'_1.e_a
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h :
  (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧
i : β✝¹
j : β✝
⊢ ⟦a✝² i * mk α✝ β✝ a✝¹ a✝⟧ + ⟦mk α✝¹ β✝¹ a✝³ a✝² * a✝ j⟧ = ⟦-a✝² i * -mk α✝ β✝ a✝¹ a✝⟧ + ⟦-mk α✝¹ β✝¹ a✝³ a✝² * -a✝ j⟧

Tactic:
congr 1

Result:
case h.e'_1.e_a.e_a
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h :
  (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧
i : β✝¹
j : β✝
⊢ ⟦a✝² i * mk α✝ β✝ a✝¹ a✝⟧ = ⟦-a✝² i * -mk α✝ β✝ a✝¹ a✝⟧

case h.e'_1.e_a.e_a
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h :
  (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧
i : β✝¹
j : β✝
⊢ ⟦mk α✝¹ β✝¹ a✝³ a✝² * a✝ j⟧ = ⟦-mk α✝¹ β✝¹ a✝³ a✝² * -a✝ j⟧

Proof state:
case h.e'_1
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h :
  (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧
i : β✝¹
j : β✝
⊢ ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveLeft (Sum.inr (i, j))⟧ =
    ⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧

Tactic:
dsimp only [mk_mul_moveLeft_inr, quot_sub, quot_add, neg_def, mulOption, moveLeft_mk]

Result:
case h.e'_1
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h :
  (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧
i : β✝¹
j : β✝
⊢ ⟦a✝² i * mk α✝ β✝ a✝¹ a✝⟧ + ⟦mk α✝¹ β✝¹ a✝³ a✝² * a✝ j⟧ - ⟦a✝² i * a✝ j⟧ =
    ⟦-a✝² i * mk β✝ α✝ (fun x => -a✝ x) fun x => -a✝¹ x⟧ + ⟦(mk β✝¹ α✝¹ (fun x => -a✝² x) fun x => -a✝³ x) * -a✝ j⟧ -
      ⟦-a✝² i * -a✝ j⟧

Proof state:
case mk.mk.mpr
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h :
  (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧
⊢ ∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).LeftMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveLeft k⟧

Tactic:
rintro (⟨i, j⟩ | ⟨i, j⟩)

Result:
case mk.mk.mpr.inl.mk
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h :
  (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧
i : α✝¹
j : α✝
⊢ P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveLeft (Sum.inl (i, j))⟧

case mk.mk.mpr.inr.mk
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h :
  (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧
i : β✝¹
j : β✝
⊢ P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveLeft (Sum.inr (i, j))⟧

Proof state:
case h.e'_1
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h :
  (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧
i : β✝¹
j : β✝
⊢ ⟦a✝² i * mk α✝ β✝ a✝¹ a✝⟧ + ⟦mk α✝¹ β✝¹ a✝³ a✝² * a✝ j⟧ - ⟦a✝² i * a✝ j⟧ =
    ⟦-a✝² i * mk β✝ α✝ (fun x => -a✝ x) fun x => -a✝¹ x⟧ + ⟦(mk β✝¹ α✝¹ (fun x => -a✝² x) fun x => -a✝³ x) * -a✝ j⟧ -
      ⟦-a✝² i * -a✝ j⟧

Tactic:
rw [← neg_def, ← neg_def]

Result:
case h.e'_1
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h :
  (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P ⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧
i : β✝¹
j : β✝
⊢ ⟦a✝² i * mk α✝ β✝ a✝¹ a✝⟧ + ⟦mk α✝¹ β✝¹ a✝³ a✝² * a✝ j⟧ - ⟦a✝² i * a✝ j⟧ =
    ⟦-a✝² i * -mk α✝ β✝ a✝¹ a✝⟧ + ⟦-mk α✝¹ β✝¹ a✝³ a✝² * -a✝ j⟧ - ⟦-a✝² i * -a✝ j⟧