@[simp]

theorem Hex.Perm.toEquiv_comm {n : ℕ} (p q : Perm n) : (p.comm q).toEquiv = ⁅p.toEquiv, q.toEquiv⁆

theorem Hex.PermGroup.Group.derived_spec {n : ℕ} (G : Group n) : closure G.derived.generators = ⁅closure G.generators, closure G.generators⁆

The checked derived group is the mathematical commutator subgroup of the ambient generated subgroup, with the original action degree retained.