Commit 2022-11-19 11:24 4fcbc82d

View on Github →

chore(data/*): Removing unnecessary simp lemmas (#17062) This PR adds a script that looks for and removes unnecessary lemmas in simp calls.

Estimated changes