Theorem: pow_mul_eq_mul_inv_cmtr_pow_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 [eq_mul_inv_iff_mul_eq, mul_assoc, ← cmtr_pow_inv_mul_eq_mul_inv_cmtr_pow, mul_inv_cancel_left]
State after:
no goals