Theorem: cycleMin_cmtr_apply_comm (Controlbits/CommutatorCycles.lean)

State before:
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
⊢ CycleMin ⁅x, y⁆ (x (y q)) = CycleMin ⁅x, y⁆ (y (x q))
Tactic:
simp_rw [cycleMin_eq_cycleMin_apply (x := y (x q)), ← Perm.mul_apply, ← mul_assoc,
  cmtr_mul_eq_mul_inv_cmtr_inv, commutatorElement_inv, Perm.mul_apply,
  cmtr_apply, inv_inv, Perm.inv_apply_self, Perm.apply_inv_self]
State after:
no goals