Commit 2022-03-11 10:13 02e0ab2c

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.