-- 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 mk.mk
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).LeftMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveLeft k⟧) ↔
    (∀ (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⟧

Tactic:
constructor <;> intro h

Result:
case mk.mk.mp
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h : ∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).LeftMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveLeft k⟧
⊢ (∀ (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⟧

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⟧

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

Tactic:
convert h.2 i j using 1

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 : β✝
⊢ ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveLeft (Sum.inr (i, j))⟧ =
    ⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧

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

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⟧

Tactic:
all_goals rw [quot_neg_mul_neg]

Result:
no goals

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

Tactic:
convert h (Sum.inr (i, j)) using 1

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

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

Tactic:
exact h.1 i j

Result:
no goals

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

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:
all_goals
  dsimp only [mk_mul_moveLeft_inr, quot_sub, quot_add, neg_def, mulOption, moveLeft_mk]
  rw [← neg_def, ← neg_def]
  congr 1
  on_goal 1 => congr 1
  all_goals rw [quot_neg_mul_neg]

Result:
no goals