simp only [Weight.sum, Function.comp_apply]
n d : ℕ
inst✝ : NeZero d
w : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ Weight.sum (Weight.comp w σ) = Weight.sum w
n d : ℕ
inst✝ : NeZero d
w : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ ∑ j : Fin (Nat.succ n), Weight.comp w σ j = ∑ j : Fin (Nat.succ n), w j