Theorem: cmtr_zpow_mul_eq_mul_inv_cmtr_zpow_inv (Controlbits/Commutator.lean)

State before:
G : Type u
inst✝ : Group G
x y : G
k : ℤ
⊢ ⁅x, y⁆ ^ k * y = y * (⁅x, y⁻¹⁆ ^ k)⁻¹
Tactic:
rw [← zpow_neg, ← cmtr_zpow_inv_mul_eq_mul_inv_cmtr_zpow, zpow_neg, inv_inv]
State after:
no goals