Theorem: cmtr_inv_apply_ne_apply_of_unfix (Controlbits/Commutator.lean)

State before:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ⁅x, y⁆⁻¹ q ≠ y q
Tactic:
simp_rw [Perm.inv_eq_iff_eq.not]
State after:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ¬q = ⁅x, y⁆ (y q)

State before:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ¬q = ⁅x, y⁆ (y q)
Tactic:
exact Ne.symm (cmtr_mul_unfix_of_unfix (x := x) hy q)
State after:
no goals