add_assoc — Mathlib

English

`(x + y) + z` has exactly the same moves as `x + (y + z)`.

Русский

Сложение слева ассоциативно: `(x + y) + z` эквивалентно `x + (y + z)`.

LaTeX

$$$ (x+y)+z \equiv x+(y+z) $$$

Lean4

/-- `(x + y) + z` has exactly the same moves as `x + (y + z)`. -/
protected theorem 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)

Похожие утверждения