mathlib

e3de4e30 - fix(algebra/direct_sum_graded): replace badly-stated and slow `simps` lemmas with manual ones (#7403)

fix(algebra/direct_sum_graded): replace badly-stated and slow `simps` lemmas with manual ones (#7403) [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/simps.20is.20very.20slow/near/236636962). The `simps mul` attribute on `direct_sum.ghas_mul.of_add_subgroups` was taking 44s, only to produce a lemma that wasn't very useful anyway. Co-authored-by: Johan Commelin <johan@commelin.net>