chore(algebra/direct_sum_graded): golf proofs (#7029)
Simplify the proofs of mul_assoc and mul_comm, and speed up all the
proofs that were slow.
Total elaboration time for this file is reduced from 12.9s to 1.7s
(on my machine), and total CPU time is reduced from 19.8s to 6.8s.
All the remaining elaboration times are under 200ms.
The main idea is to explicitly construct bundled homomorphisms
corresponding to `λ a b c, a * b * c` and `λ a b c, a * (b * c)`
respectively. Then in proving the equality between those, we can
unpack all the arguments immediately, and the remaining rewrites
needed become simpler.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
