simp only [Weight.comp, Equiv.Perm.coe_mul]
n d : ℕ
inst✝ : NeZero d
w : Weight n d
σ τ : Equiv.Perm (Fin (Nat.succ n))
⊢ Weight.comp (Weight.comp w σ) τ = Weight.comp w (σ * τ)
n d : ℕ
inst✝ : NeZero d
w : Weight n d
σ τ : Equiv.Perm (Fin (Nat.succ n))
⊢ (w ∘ ⇑σ) ∘ ⇑τ = w ∘ ⇑σ ∘ ⇑τ