Theorem: mul_inv_cmtr_inv_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 [← cmtr_mul_eq_mul_inv_cmtr_inv]
State after:
α : Type u
x y : Perm α
q : α
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ * y) q ≠ q

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