-- 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.mp.left
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:
exact h (Sum.inl (i, j))

Result:
no goals

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

Tactic:
cases y

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

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⟧

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:
on_goal 1 => 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⟧

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 * a✝ j⟧ = ⟦-a✝² i * -a✝ j⟧

Tactic:
rw [quot_neg_mul_neg]

Result:
no goals

Proof state:
x y : PGame
P : Game → Prop
⊢ (∀ (k : (x * y).LeftMoves), P ⟦(x * y).moveLeft k⟧) ↔
    (∀ (i : x.LeftMoves) (j : y.LeftMoves), P ⟦x.mulOption y i j⟧) ∧
      ∀ (i : (-x).LeftMoves) (j : (-y).LeftMoves), P ⟦(-x).mulOption (-y) i j⟧

Tactic:
cases x

Result:
case mk
y : PGame
P : Game → Prop
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (∀ (k : (mk α✝ β✝ a✝¹ a✝ * y).LeftMoves), P ⟦(mk α✝ β✝ a✝¹ a✝ * y).moveLeft k⟧) ↔
    (∀ (i : (mk α✝ β✝ a✝¹ a✝).LeftMoves) (j : y.LeftMoves), P ⟦(mk α✝ β✝ a✝¹ a✝).mulOption y i j⟧) ∧
      ∀ (i : (-mk α✝ β✝ a✝¹ a✝).LeftMoves) (j : (-y).LeftMoves), P ⟦(-mk α✝ β✝ a✝¹ a✝).mulOption (-y) i j⟧

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

Tactic:
constructor <;> intros i j

Result:
case mk.mk.mp.left
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⟧

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⟧