negMulRelabelling — Mathlib

Lean4
/-- `-x * y` and `-(x * y)` have the same moves. -/
def negMulRelabelling (x y : PGame.{u}) : -x * y ≡r -(x * y) :=
  match x, y with
  | ⟨xl, xr, xL, xR⟩, ⟨yl, yr, yL, yR⟩ => by
    refine ⟨Equiv.sumComm _ _, Equiv.sumComm _ _, ?_, ?_⟩ <;> rintro (⟨i, j⟩ | ⟨i, j⟩) <;>
      · dsimp
        apply ((negAddRelabelling _ _).trans _).symm
        apply ((negAddRelabelling _ _).trans (Relabelling.addCongr _ _)).subCongr
        · exact (negMulRelabelling _ _).symm
        · exact (negMulRelabelling _ _).symm
        change -(mk xl xr xL xR * _) ≡r _
        exact (negMulRelabelling _ _).symm
termination_by (x, y)
Похожие утверждения