Commit 2021-03-05 05:37 340dd69f

fix(*): remove some simp lemmas (#6541) All of these simp lemmas are also declared in core. Maybe one of the copies can be removed in a future PR, but this PR is just to remove the duplicate simp attributes. This is part of fixing linting problems in core, done in leanprover-community/lean#545. Most of the duplicate simp lemmas are fixed in core, but I prefer to remove the simp attribute here in mathlib if the simp lemmas were already used in core.