Theorem: cmtr_zpow_apply_ne_apply_cmtr_pow_apply (Controlbits/Commutator.lean)

State before:
α : Type u
x y : Perm α
q : α
j k : ℤ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (⁅x, y⁆ ^ j) q ≠ y ((⁅x, y⁆ ^ k) q)
Tactic:
rw [← sub_add_cancel j k, zpow_add, Perm.mul_apply]
State after:
α : Type u
x y : Perm α
q : α
j k : ℤ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (⁅x, y⁆ ^ (j - k)) ((⁅x, y⁆ ^ k) q) ≠ y ((⁅x, y⁆ ^ k) q)

State before:
α : Type u
x y : Perm α
q : α
j k : ℤ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (⁅x, y⁆ ^ (j - k)) ((⁅x, y⁆ ^ k) q) ≠ y ((⁅x, y⁆ ^ k) q)
Tactic:
exact cmtr_zpow_apply_ne_apply hxy hy
State after:
no goals