refactor(group_theory/commutator): Golf some proofs (#12586)
This PR golfs the proofs of some lemmas in `commutator.lean`.
I also renamed `bot_commutator` and `commutator_bot` to `commutator_bot_left` and `commutator_bot_right`, since "bot_commutator" didn't sound right to me (you would say "the commutator of H and K", not "H commutator K"), but I can revert to the old name if you want.
