mathlib

30abde68 - chore(*): clean up some unused open statements and extra simps (#10342)

chore(*): clean up some unused open statements and extra simps (#10342) We clean up some specific statements that are essentially no-ops in the library, i.e. opening a namespace and then never using it and using a simp-set larger than actually needed. This is a preparatory miscellany of small fixes for a larger PR upcoming from me and Johan to reduce imports in the library. Hopefully merging this first will make the content of that PR clearer. Co-authored-by: Johan Commelin <johan@commelin.net>