Symmetric-group relabelling action on ordered configurations

import Mathlib
import Definitions.Def_BraidsLinksMCG_ConfigSpace

namespace TarchaBraids

open BraidsLinksMCG

def orderedConfigPermute {n : ℕ} (g : Equiv.Perm (Fin n)) (p : OrderedConfig n) :
    OrderedConfig n :=
  ⟨p.1 ∘ g.symm, p.2.comp g.symm.injective⟩

instance orderedConfigPermMulAction (n : ℕ) :
    MulAction (Equiv.Perm (Fin n)) (OrderedConfig n) where
  smul g p := orderedConfigPermute g p
  one_smul p := by
    apply Subtype.ext
    rfl
  mul_smul g h p := by
    apply Subtype.ext
    rfl

instance orderedConfigPermContinuous (n : ℕ) :
    ContinuousConstSMul (Equiv.Perm (Fin n)) (OrderedConfig n) where
  continuous_const_smul g := by
    apply Continuous.subtype_mk
    exact continuous_pi fun i =>
      (continuous_apply (g.symm i)).comp continuous_subtype_val

end TarchaBraids