Theorem: cmtr_zpow_apply_ne_apply (Controlbits/Commutator.lean)

State before:
α : Type u
x y : Perm α
q : α
k : ℤ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (⁅x, y⁆ ^ k) q ≠ y q
Tactic:
cases k
State after:
case ofNat
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
a✝ : ℕ
⊢ (⁅x, y⁆ ^ Int.ofNat a✝) q ≠ y q

case negSucc
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
a✝ : ℕ
⊢ (⁅x, y⁆ ^ Int.negSucc a✝) q ≠ y q

State before:
case ofNat
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
a✝ : ℕ
⊢ (⁅x, y⁆ ^ Int.ofNat a✝) q ≠ y q
Tactic:
simp only [Int.ofNat_eq_coe, zpow_natCast, ne_eq, hxy, hy, not_false_eq_true, implies_true,
  cmtr_pow_apply_ne_apply]
State after:
no goals

State before:
case negSucc
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
a✝ : ℕ
⊢ (⁅x, y⁆ ^ Int.negSucc a✝) q ≠ y q
Tactic:
simp only [zpow_negSucc, ne_eq, hxy, hy, not_false_eq_true, implies_true,
  cmtr_pow_inv_apply_ne_apply]
State after:
no goals