mathlib3

4fcbc82d - chore(data/*): Removing unnecessary simp lemmas (#17062)

chore(data/*): Removing unnecessary simp lemmas (#17062) This PR adds a script that looks for and removes unnecessary lemmas in simp calls. - [x] depends on: #17078