Theorem: cmtr_mul_unfix_of_unfix (Controlbits/Commutator.lean)

State before:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ * y) q ≠ q
Tactic:
simp_rw [Perm.mul_apply, cmtr_apply, Perm.inv_apply_self, ← Perm.eq_inv_iff_eq (f := x).not]
State after:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), ¬y (x⁻¹ q) = x⁻¹ q

State before:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), ¬y (x⁻¹ q) = x⁻¹ q
Tactic:
exact fun q => hy (x⁻¹ q)
State after:
no goals