instMul — Mathlib

Lean4
/-- The product of `x = {xL | xR}` and `y = {yL | yR}` is
`{xL*y + x*yL - xL*yL, xR*y + x*yR - xR*yR | xL*y + x*yR - xL*yR, xR*y + x*yL - xR*yL}`. -/
instance : Mul PGame.{u} :=
  ⟨fun x y =>
    by
    induction x generalizing y with
    | mk xl xr _ _ IHxl IHxr => _
    induction y with
    | mk yl yr yL yR IHyl IHyr => _
    have y := mk yl yr yL yR
    refine ⟨(xl × yl) ⊕ (xr × yr), (xl × yr) ⊕ (xr × yl), ?_, ?_⟩ <;> rintro (⟨i, j⟩ | ⟨i, j⟩)
    · exact IHxl i y + IHyl j - IHxl i (yL j)
    · exact IHxr i y + IHyr j - IHxr i (yR j)
    · exact IHxl i y + IHyr j - IHxl i (yR j)
    · exact IHxr i y + IHyl j - IHxr i (yL j)⟩
Похожие утверждения