Step compatibility of the colouring conjugation

The conjugation of a whiskered endomorphism into the colouring model equals the colour-extension of the conjugate: unwinding colourPowerEquiv (n + 1) as tensorCongr.trans step and observing that the tensorCongr-conjugation of a whisker is tensorHom of the inner conjugation.

theorem RS.toColour_whisker {k ℓ : ℕ} (n : ℕ) (g : superPow (stdSuperPair k ℓ) n ⟶ superPow (stdSuperPair k ℓ) n) : toColour (n + 1) (CategoryTheory.MonoidalCategoryStruct.whiskerRight g (stdSuperPair k ℓ)) = colourExtend n (toColour n g)

The step compatibility: conjugating a whiskered endomorphism into the colouring model extends the conjugate.