Theorem: mul_cmtr_unfix_of_unfix (Controlbits/Commutator.lean)

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

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