mathlib3

355472dc - refactor(group_theory/commutator): Golf proof of `commutator_mem_commutator` (#12584)

refactor(group_theory/commutator): Golf proof of `commutator_mem_commutator` (#12584) This PR golfs the proof of `commutator_mem_commutator`, and moves it earlier in the file so that it can be used earlier.