Theorem: cmtr_pow_inv_mul_eq_mul_inv_cmtr_pow (Controlbits/Commutator.lean)

State before:
G : Type u
inst✝ : Group G
x y : G
k : ℕ
⊢ (⁅x, y⁆ ^ k)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ k
Tactic:
induction' k with n hn
State after:
case zero
G : Type u
inst✝ : Group G
x y : G
⊢ (⁅x, y⁆ ^ 0)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ 0

case succ
G : Type u
inst✝ : Group G
x y : G
n : ℕ
hn : (⁅x, y⁆ ^ n)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ n
⊢ (⁅x, y⁆ ^ (n + 1))⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ (n + 1)

State before:
case zero
G : Type u
inst✝ : Group G
x y : G
⊢ (⁅x, y⁆ ^ 0)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ 0
Tactic:
simp_rw [pow_zero, inv_one, mul_one, one_mul]
State after:
no goals

State before:
case succ
G : Type u
inst✝ : Group G
x y : G
n : ℕ
hn : (⁅x, y⁆ ^ n)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ n
⊢ (⁅x, y⁆ ^ (n + 1))⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ (n + 1)
Tactic:
simp_rw [pow_succ ⁅x, y⁻¹⁆, pow_succ' ⁅x, y⁆, ← mul_assoc, hn.symm, mul_inv_rev, mul_assoc,
  cmtr_inv_mul_eq_mul_inv_cmtr]
State after:
no goals