chore(*): miscellaneous to_additive related cleanup (#11316)
A few cleanup changes related to to_additive:
* After https://github.com/leanprover-community/lean/pull/618 was merged, we no longer need to add namespaces manually in filtered_colimits and open subgroup
* to_additive can now generate some more lemmas in big_operators/fin
* to_additive now handles a proof in measure/haar better than it used to
so remove a workaround there
