The bit I like most about it is how it actually uses the fact that the group of permutations acting on itself always yields isomorphism. This may sounds like a stupidly elementary fact about group theory, but it's just not a thing that I've had to use very often in manipulating expressions with pis and sigmas.
It comes up because I'm summing twice over all permutations of an m-element set, and then considering a product over all elements in that set, so like
sum_{rho in S_m} sum_{pi in S_m} prod_{j in 1..m} f(j, pi j, rho j)
There's one kind of reindexing that I am somewhat used to, which is replacing j with an expression like rho^-1 k to get
sum_{rho in S_m} sum_{pi in S_m} prod_{rho^-1 k in 1..m} f(rho^-1 k, pi rho^-1 k, k)
and using the fact that rho is an isomorphism acting on the set 1..m to drop the rho^-1 from the product:
sum_{rho in S_m} sum_{pi in S_m} prod_{rho^-1 k in 1..m} f(rho^-1 k, pi rho^-1 k, k)
The extra neat thing is exactly that you can do a substitution 'one level up' and say pi = zeta o rho
sum_{rho in S_m} sum_{(zeta o rho) in S_m} prod_{rho^-1 k in 1..m} f(rho^-1 k, zeta k, k)
and reason that since rho acting on S_m is an isomorphism, you might as well say
sum_{rho in S_m} sum_{zeta in S_m} prod_{rho^-1 k in 1..m} f(rho^-1 k, zeta k, k)
