mathlib
b89df0ab - chore(set_theory/pgame): remove redundant `dsimp` (#15312)

Commit

3 years ago

chore(set_theory/pgame): remove redundant `dsimp` (#15312) Thanks to #14660, we no longer need the `dsimp, simp` pattern to prove some results.

Author

vihdzp

Parents