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