mathlib

84a27d60 - feat(set_theory/game): add mul_one and mul_assoc for pgames (#7610)

feat(set_theory/game): add mul_one and mul_assoc for pgames (#7610) and several `simp` lemmas. I also simplified some of the existing proofs using `rw` and `simp` and made them easier to read. This is the final PR for multiplication of pgames (hopefully)! Next step: prove `numeric_mul` and define multiplication for `surreal`.