Theorem: cmtr_pow_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:
simp_rw [← Perm.eq_inv_iff_eq.not, ← Perm.mul_apply, cmtr_pow_inv_mul_eq_mul_inv_cmtr_pow, hxy]
State after:
α : Type u
x y : Perm α
q : α
k : ℕ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ¬q = (y * ⁅x, y⁆ ^ k) q

State before:
α : Type u
x y : Perm α
q : α
k : ℕ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ¬q = (y * ⁅x, y⁆ ^ k) q
Tactic:
exact Ne.symm (mul_cmtr_pow_unfix hxy hy _)
State after:
no goals