Theorem: cmtr_mul_eq_mul_inv_cmtr_inv (Controlbits/Commutator.lean)

State before:
G : Type u
inst✝ : Group G
x y : G
⊢ ⁅x, y⁆ * y = y * ⁅x, y⁻¹⁆⁻¹
Tactic:
simp_rw [commutatorElement_inv, commutatorElement_def, inv_mul_cancel_right,
  mul_assoc, mul_inv_cancel_left, inv_inv]
State after:
no goals