-- Mathlib/SetTheory/Game/PGame.lean
/-- `(x + y) + z` has exactly the same moves as `x + (y + z)`. -/
protected lemma add_assoc (x y z : PGame) : x + y + z ≡ x + (y + z) :=
  match x, y, z with
  | mk xl xr xL xR, mk yl yr yL yR, mk zl zr zL zR => by
    refine Identical.of_equiv (Equiv.sumAssoc _ _ _) (Equiv.sumAssoc _ _ _) ?_ ?_ <;>
    · rintro ((_ | _) | _)
      · exact PGame.add_assoc _ _ _
      · exact PGame.add_assoc (mk _ _ _ _) _ _
      · exact PGame.add_assoc (mk _ _ _ _) (mk _ _ _ _) _
  termination_by (x, y, z)

Proof state:
case refine_2.inl.inr
x y z : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
val✝ : yr
⊢ (mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inl (Sum.inr val✝)) ≡
    (mk xl xr xL xR + (mk yl yr yL yR + mk zl zr zL zR)).moveRight ((Equiv.sumAssoc xr yr zr) (Sum.inl (Sum.inr val✝)))

Tactic:
exact PGame.add_assoc (mk _ _ _ _) _ _

Result:
no goals

Proof state:
case refine_2.inl.inl
x y z : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
val✝ : xr
⊢ (mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inl (Sum.inl val✝)) ≡
    (mk xl xr xL xR + (mk yl yr yL yR + mk zl zr zL zR)).moveRight ((Equiv.sumAssoc xr yr zr) (Sum.inl (Sum.inl val✝)))

Tactic:
exact PGame.add_assoc _ _ _

Result:
no goals

Proof state:
case refine_2
x y z : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
⊢ ∀ (i : (mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR).RightMoves),
    (mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR).moveRight i ≡
      (mk xl xr xL xR + (mk yl yr yL yR + mk zl zr zL zR)).moveRight ((Equiv.sumAssoc xr yr zr) i)

Tactic:
rintro ((_ | _) | _)

Result:
case refine_2.inl.inl
x y z : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
val✝ : xr
⊢ (mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inl (Sum.inl val✝)) ≡
    (mk xl xr xL xR + (mk yl yr yL yR + mk zl zr zL zR)).moveRight ((Equiv.sumAssoc xr yr zr) (Sum.inl (Sum.inl val✝)))

case refine_2.inl.inr
x y z : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
val✝ : yr
⊢ (mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inl (Sum.inr val✝)) ≡
    (mk xl xr xL xR + (mk yl yr yL yR + mk zl zr zL zR)).moveRight ((Equiv.sumAssoc xr yr zr) (Sum.inl (Sum.inr val✝)))

case refine_2.inr
x y z : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
val✝ : zr
⊢ (mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inr val✝) ≡
    (mk xl xr xL xR + (mk yl yr yL yR + mk zl zr zL zR)).moveRight ((Equiv.sumAssoc xr yr zr) (Sum.inr val✝))

Proof state:
case refine_2.inr
x y z : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
zl zr : Type u_1
zL : zl → PGame
zR : zr → PGame
val✝ : zr
⊢ (mk xl xr xL xR + mk yl yr yL yR + mk zl zr zL zR).moveRight (Sum.inr val✝) ≡
    (mk xl xr xL xR + (mk yl yr yL yR + mk zl zr zL zR)).moveRight ((Equiv.sumAssoc xr yr zr) (Sum.inr val✝))

Tactic:
exact PGame.add_assoc (mk _ _ _ _) (mk _ _ _ _) _

Result:
no goals