Theorem: cmtr_zpow_inv_mul_eq_mul_inv_cmtr_zpow (Controlbits/Commutator.lean)

State before:
G : Type u
inst✝ : Group G
x y : G
k : ℤ
⊢ (⁅x, y⁆ ^ k)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ k
Tactic:
cases k
State after:
case ofNat
G : Type u
inst✝ : Group G
x y : G
a✝ : ℕ
⊢ (⁅x, y⁆ ^ Int.ofNat a✝)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ Int.ofNat a✝

case negSucc
G : Type u
inst✝ : Group G
x y : G
a✝ : ℕ
⊢ (⁅x, y⁆ ^ Int.negSucc a✝)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ Int.negSucc a✝

State before:
case ofNat
G : Type u
inst✝ : Group G
x y : G
a✝ : ℕ
⊢ (⁅x, y⁆ ^ Int.ofNat a✝)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ Int.ofNat a✝
Tactic:
simp only [Int.ofNat_eq_coe, zpow_natCast, zpow_neg, cmtr_pow_inv_mul_eq_mul_inv_cmtr_pow]
State after:
no goals

State before:
case negSucc
G : Type u
inst✝ : Group G
x y : G
a✝ : ℕ
⊢ (⁅x, y⁆ ^ Int.negSucc a✝)⁻¹ * y = y * ⁅x, y⁻¹⁆ ^ Int.negSucc a✝
Tactic:
simp only [zpow_negSucc, zpow_neg, inv_inv, pow_mul_eq_mul_inv_cmtr_pow_inv]
State after:
no goals