Theorem: cmtr_pow_inv_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.inv_eq_iff_eq.not]
State after:
α : Type u
x y : Perm α
q : α
k : ℕ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ¬q = (⁅x, y⁆ ^ k) (y q)

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