Theorem: cmtr_inv_mul_eq_mul_inv_cmtr (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_inv, mul_assoc]
State after:
no goals